An implementation model of the typed λ-calculus based on Linear Chemical Abstract Machine

Shinya Sato, Toru Sugimoto, Shinichi Yamada

研究成果: Conference article査読

抄録

Abramsky's Linear Chemical Abstract Machine is a term calculus which corresponds to Linear Logic, via the Curry-Howard isomorphism. We show that the typed λ-calculus is embedded into Linear Chemical Abstract Machine by Girard's embedding of Intuitionistic Logic into Linear Logic. Then we extend our result to a simple functional programming language obtained from the typed λ-calculus by adding constants from PCF. We show that the call-by-value evaluation of terms of ground types (Booleans and Natural numbers) are preserved and reflected by this translation. Finally, we discuss an operational perspective of our result. We give a sequential execution model of Linear CHAM based on Abramsky's idea of a stack of coequations and a name queue, and then we consider a concurrent multi-thread implementation of the model.

本文言語English
ページ(範囲)292-307
ページ数16
ジャーナルElectronic Notes in Theoretical Computer Science
64
DOI
出版ステータスPublished - 2002 9
外部発表はい

ASJC Scopus subject areas

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

フィンガープリント

「An implementation model of the typed λ-calculus based on Linear Chemical Abstract Machine」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル