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.

Short bio

Chung-Kil Hur receives his PhD degree in Computer Science from Computer Laboratory at Univerity of Cambridge in 2009. He is working as a postdoc at Laboratoire Preuves, Programmes et Systemes (PPS) in Paris from Nov 2009. His research interest includes category theory, especially categorical algebra; equational logic and term rewriting; logical relation and compiler correctness. He has B.S. in Computer Science and Mathematics (both Magna Cum Laude) from KAIST, and is a bronze medalist in the 35th International Mathematical Olympiad.

Resources

• talk slide