A study of abramsky’s linear chemical abstract machine

Seikoh Mikami, Yohji Akama

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Abramsky’s Linear Chemical Abstract Machine (lcham) is a term calculus which corresponds to Linear Logic, via the Curry-Howard isomorphism. We introduce a translation from a linear λcalculus into lcham. The translation result can be well regarded as a black box with the i/o ports being atomic.We show that one step computation of lcham is equivalent to that of the linear λcalculus. Then, we prove the principal typing theorem of lcham, which implies the decidability of type checking.

Original languageEnglish
Title of host publicationTyped Lambda Calculi and Applications - 4th International Conference, TLCA 1999, Proceedings
EditorsJean-Yves Girard
PublisherSpringer Verlag
Pages243-257
Number of pages15
ISBN (Print)3540657630, 9783540657637
DOIs
Publication statusPublished - 1999
Event4th International Conference on Typed Lambda Calculi and Applications, TLCA 1999 - L’Aquila, Italy
Duration: 1999 Apr 71999 Apr 9

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1581
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other4th International Conference on Typed Lambda Calculi and Applications, TLCA 1999
CountryItaly
CityL’Aquila
Period99/4/799/4/9

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A study of abramsky’s linear chemical abstract machine'. Together they form a unique fingerprint.

Cite this