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.
|ジャーナル||Conference Record of the Annual ACM Symposium on Principles of Programming Languages|
|出版ステータス||Published - 2005|
|イベント||POPL 2005: The 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - Long Beach, CA, United States|
継続期間: 2005 1 12 → 2005 1 14
ASJC Scopus subject areas