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.