Title: 

Observational equivalence on low-level programs and compositional compiler correctness

Abstract: 

Giving a good notion of observational equivalence on low-level
programs is particularly difficult due to the presence of
non-functional operations such as those examining instructions of
function closures.  In the talk, 
(1) I discuss this difficulty by giving instructive examples in 
    the untyped lambda calculus extended with the operation that 
    tests alpha-equality of two terms; 
(2) give a notion of equivalence on those lambda terms by means of 
    logical relation equipped with step-indexing and biorthogonality;
(3) explain how to use this relation to give a compositional notion of
    correctness of compilers and hand-optimizations;
(4) and finally discuss limitations of step-indexing and future work.

These results have been fully formalized using the Coq proof assistant.

This is joint work with Nick Benton.