Typed Normal Form Bisimulation for Parametric Polymorphism
Venue
Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science (LICS' 08), IEEE (2008), pp. 341-352
Publication Year
2008
Authors
Soren B. Lassen, Paul Blain Levy
BibTeX
Abstract
This paper presents a new bisimulation theory for parametric polymorphism which
enables straightforward co-inductive proofs of program equivalences involving
existential types. The theory is an instance of typed normal form bisimulation and
demonstrates the power of this recent framework for modeling typed lambda calculi
as labelled transition systems. We develop our theory for a continuation-passing
style calculus, Jump-With-Argument, where normal form bisimulation takes a simple
form. We equip the calculus with both existential and recursive types. An "ultimate
pattern matching theorem" enables us to define bisimilarity and we show it to be a
congruence. We apply our theory to proving program equivalences, type isomorphisms
and genericity.
