A study of abramsky’s linear chemical abstract machine

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.