Google Research

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


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.

Learn more about how we do research

We maintain a portfolio of research projects, providing individuals and teams the freedom to emphasize specific types of work