Title:

Logical relations and compositional compiler correctness

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.