Title:

Compiler correctness and observational equivalence on machine code

Abstract:

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 step-indexing,
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.

This is joint work with Nick Benton.