Biorthogonality, step-indexing and compiler correctness

11 years 11 months ago
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...
Nick Benton, Chung-Kil Hur
Added 22 Nov 2009
Updated 22 Nov 2009
Type Conference
Year 2009
Where ICFP
Authors Nick Benton, Chung-Kil Hur
Comments (0)