Logical Relations and Compositional Compiler Correctness Seminars/Workshops

Abstract

We define operational logical relations between terms of a polymorphically typed functional language and low-level programs for a variant SECD machine. The relations, defined using relational parametricity, biorthogonality and step-indexing, give extensional and compositional specifications that capture what it means for low-level code and machine values to realize typed source-level terms. We show how the relations can be used to establish not only a traditional form of compiler correctness, but also to justify linking compiled code with code from elsewhere such as library routine and hand-optimized code fragments that exploit non-parametric and non-functional low-level operations, yet are extensionally well-behaved.

The definitions and results have been fully formalized using the Coq proof assistant.

This is joint work with Nick Benton.