A Bisimulation for Type Abstraction and Recursion
Files
Related Collections
Degree type
Discipline
Subject
Contextual Equivalence
Bisimulations
Logical Relations
Existential Types
Recursive Types
Funder
Grant number
License
Copyright date
Distributor
Related resources
Author
Contributor
Abstract
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.
Advisor
Date of presentation
Conference name
Conference dates
Conference location
Date Range for Data Collection (Start Date)
Date Range for Data Collection (End Date)
Digital Object Identifier
Series name and number
Volume number
Issue number
Publisher
Publisher DOI
Comments
Postprint version. Copyright ACM, 2005. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2005, pages 63-74. Publisher URL: http://doi.acm.org/10.1145/1040305.1040311
Postprint version. Copyright ACM, 2005. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages 2005, pages 63-74. Publisher URL: http://doi.acm.org/10.1145/1040305.1040311