TY - GEN
T1 - A study of abramsky’s linear chemical abstract machine
AU - Mikami, Seikoh
AU - Akama, Yohji
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1999.
PY - 1999
Y1 - 1999
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84949205776&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84949205776&partnerID=8YFLogxK
U2 - 10.1007/3-540-48959-2_18
DO - 10.1007/3-540-48959-2_18
M3 - Conference contribution
AN - SCOPUS:84949205776
SN - 3540657630
SN - 9783540657637
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 243
EP - 257
BT - Typed Lambda Calculi and Applications - 4th International Conference, TLCA 1999, Proceedings
A2 - Girard, Jean-Yves
PB - Springer Verlag
T2 - 4th International Conference on Typed Lambda Calculi and Applications, TLCA 1999
Y2 - 7 April 1999 through 9 April 1999
ER -