Logical bisimulations and functional languages

Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii

研究成果: Conference contribution

8 被引用数 (Scopus)

抄録

Developing a theory of bisimulation in higher-order languages can be hard. Particularly challenging can be the proof of congruence and, related to this, enhancements of the bisimulation proof method with "up-to context" techniques. We present logical bisimulations, a form of bisimulation for higherorder languages, in which the bisimulation clause is somehow reminiscent of logical relations. We consider purely functional languages, in particular untyped call-by-name and call-by-value lambda-calculi, and, in each case: we present the basic properties of logical bisimilarity, including congruence; we show that it coincides with contextual equivalence; we develop some up-to techniques, including up-to context, as examples of possible enhancements of the associated bisimulation method.

本文言語English
ホスト出版物のタイトルInternational Symposium on Fundamentals of Software Engineering - International Symposium, FSEN 2007, Proceedings
ページ364-379
ページ数16
出版ステータスPublished - 2007 12 1
イベント2nd IPM International Symposium on Fundamentals of Software Engineering, FSEN 2007 - Tehran, Iran, Islamic Republic of
継続期間: 2007 4 172007 4 19

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
4767 LNCS
ISSN(印刷版)0302-9743
ISSN(電子版)1611-3349

Other

Other2nd IPM International Symposium on Fundamentals of Software Engineering, FSEN 2007
国/地域Iran, Islamic Republic of
CityTehran
Period07/4/1707/4/19

ASJC Scopus subject areas

  • 理論的コンピュータサイエンス
  • コンピュータ サイエンス(全般)

フィンガープリント

「Logical bisimulations and functional languages」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル