Typed Normal Form Bisimulation for Parametric Polymorphism
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.
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.
Research Areas
