Biorthogonality, step-indexing and compiler correctness

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 stepindexing, 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. Categories and Subject Descriptors F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs--Mechanical verification, Specification techniques; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages--Denotational semantics, Operational semantics; F.3.3 [Logics and Meanings of Programs]: Studies of Program Constructs--Type structure,Functional constructs; D.3.4 [Programming Languages]: Processors--Compilers; D.2.4 [Software Engineering]: Softwar...

• Type: Conference
• Year: 2009
• Where: ICFP
• Authors: Nick Benton, Chung-Kil Hur
• Keywords: Denotational Semantics, ICFP 2009, Operational Semantics, Programming Languages, Verification Keywords Compiler