Typed Normal Form Bisimulation for Parametric Polymorphism

Soren B. Lassen
Paul Blain Levy
Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science (LICS' 08), IEEE (2008), pp. 341-352

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.