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

Shinya Sato, Tooru Sugimoto, Shinichi Yamada

Research output: Contribution to journalArticle

Abstract

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.

Original languageEnglish
Pages (from-to)301-316
Number of pages16
JournalElectronic Notes in Theoretical Computer Science
Volume64
DOIs
Publication statusPublished - 2002 Sep
Externally publishedYes

Fingerprint

Functional programming
Computer programming languages

ASJC Scopus subject areas

  • Computer Science (miscellaneous)

Cite this

An implementation model of the typed λ-calculus based on Linear Chemical Abstract Machine. / Sato, Shinya; Sugimoto, Tooru; Yamada, Shinichi.

In: Electronic Notes in Theoretical Computer Science, Vol. 64, 09.2002, p. 301-316.

Research output: Contribution to journalArticle

@article{1976ed775676466e8579cf9719c5dc6d,
title = "An implementation model of the typed λ-calculus based on Linear Chemical Abstract Machine",
abstract = "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.",
author = "Shinya Sato and Tooru Sugimoto and Shinichi Yamada",
year = "2002",
month = "9",
doi = "10.1016/S1571-0661(04)80356-6",
language = "English",
volume = "64",
pages = "301--316",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",

}

TY - JOUR

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

AU - Sato, Shinya

AU - Sugimoto, Tooru

AU - Yamada, Shinichi

PY - 2002/9

Y1 - 2002/9

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=18944370369&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=18944370369&partnerID=8YFLogxK

U2 - 10.1016/S1571-0661(04)80356-6

DO - 10.1016/S1571-0661(04)80356-6

M3 - Article

VL - 64

SP - 301

EP - 316

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -