A bisimulation for type abstraction and recursion

Eijiro Sumii, Benjamin C. Pierce

研究成果: Conference article査読

11 被引用数 (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.

本文言語English
ページ(範囲)63-74
ページ数12
ジャーナルConference Record of the Annual ACM Symposium on Principles of Programming Languages
DOI
出版ステータスPublished - 2005
外部発表はい
イベントPOPL 2005: The 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - Long Beach, CA, United States
継続期間: 2005 1 122005 1 14

ASJC Scopus subject areas

  • ソフトウェア

フィンガープリント

「A bisimulation for type abstraction and recursion」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル