A bisimulation for type abstraction and recursion

Eijiro Sumii, Benjamin C. Pierce

研究成果: Article査読

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

本文言語English
論文番号26
ジャーナルJournal of the ACM
54
5
DOI
出版ステータスPublished - 2007 10 1

ASJC Scopus subject areas

  • ソフトウェア
  • 制御およびシステム工学
  • 情報システム
  • ハードウェアとアーキテクチャ
  • 人工知能

フィンガープリント

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

引用スタイル