Paper: Typed Normal Form Bisimulation for Parametric Polymorphism (at LICS 2008)

Authors: Soren B. Lassen Paul Blain Levy

Abstract

This paper presents a new bisimulation theory for parametric polymorphism which enables straight forward 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.

BibTeX

  @InProceedings{LassenLevy-TypedNormalFormBisi,
    author = 	 {Soren B. Lassen and Paul Blain Levy},
    title = 	 {Typed Normal Form Bisimulation for Parametric Polymorphism},
    booktitle =  {Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science (LICS 2008)},
    year =	 {2008},
    month =	 {June}, 
    pages =      {341--352},
    location =   {Pittsburgh, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }