 |
Biorthogonality, Step-Indexing and Compiler Correctness
Nick Benton and Chung-Kil Hur
The 14th ACM SIGPLAN International Conference on Functional Programming (ICFP 2009)Edinburgh, Scotland, 31st August - 2nd September 2009
Abstract
We define logical relations between the denotational semantics of a simply typed functional language with recursion and the operational behaviour of low-level programs in a variant SECD machine. The relations, which are defined using biorthogonality and step-indexing, capture what it means for a piece of low-level code to implement a mathematical, domain-theoretic function and are used to prove correctness of a simple compiler. The results have been formalized in the Coq proof assistant.
START Conference Manager (V2.56.8 - Rev. 748M)