A bisimulation for type abstraction and recursion

Eijiro Sumii, Benjamin C. Pierce

Research output: Contribution to journalConference articlepeer-review

14 Citations (Scopus)


We present a sound, complete, and elementary proof method, based on bisimulation, for contextual equivalence in a λ-calculus with full universal, existential, and recursive types. Unlike logical relations (either semantic or syntactic), our development is elementary, using only sets and relations and avoiding advanced machinery such as domain theory, admissibility, and TT -closure. Unlike other bisimulations, ours is complete even for existential types. The key idea is to consider sets of relations - instead of just relations - as bisimulations.

Original languageEnglish
Pages (from-to)63-74
Number of pages12
JournalConference Record of the Annual ACM Symposium on Principles of Programming Languages
Publication statusPublished - 2005
Externally publishedYes
EventPOPL 2005: The 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - Long Beach, CA, United States
Duration: 2005 Jan 122005 Jan 14


  • Bisimulations
  • Contextual Equivalence
  • Existential Types
  • Lambda-Calculus
  • Logical Relations
  • Recursive Types

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'A bisimulation for type abstraction and recursion'. Together they form a unique fingerprint.

Cite this