Date: Wed 7 Feb
Time: 15.00
Place: room 214

Speaker: Andrew M. Pitts (Cambridge Univ.)
Title: Operationally-based logical relations for idealized Algol
Reference: Eugenio Moggi e Pino Rosolini

Abstract. I will present a notion of logical relation for Idealized Algol (IA) which is parameterized by "relations-with-divergence" between states. It yields an applicative characterization of contextual equivalence for IA and provides a relatively straightforward method for establishing some of the equivalences that have been considered in the literature - including those which hinge upon the undefinability of "snapback" in IA. The definition of the logical relation was inspired by recent work of O'Hearn and Reynolds (on translating IA into a predicatively polymorphic linear lambda calculus). The hard work in the operational version lies in establishing the "fundamental theorem of logical relations" for this logical relation. The proof makes use of a compactness property of fixpoint recursion with respect to evaluation of IA phrases.