An implementation model of the typed lambda-calculus based on Linear Chemical Abstract Machine
Shinya Sato, Toru Sugimoto and Shinichi Yamada
In Proc. of the International Workshop on Functional and (Constraint) Logic Programming (WFLP 2001)
, Report No. 2017, University of Kiel
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 lambda-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 lambda-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.