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.