A bisimulation for type abstraction and recursion

Eijiro Sumii, Benjamin C. Pierce

Research output: Contribution to journalArticlepeer-review

44 Citations (Scopus)


We present a bisimulation method for proving the contextual equivalence of packages in -calculus with full existential and recursive types. Unlike traditional 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
Article number26
JournalJournal of the ACM
Issue number5
Publication statusPublished - 2007 Oct 1


  • Bisimulations
  • Contextual equivalence
  • Existential types
  • Lambda-calculus
  • Logical relations
  • Recursive types

ASJC Scopus subject areas

  • Software
  • Control and Systems Engineering
  • Information Systems
  • Hardware and Architecture
  • Artificial Intelligence


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

Cite this