The Linear Logical Abstract Machine

Abstract

We derive an abstract machine from the Curry-Howard correspondence with a sequent calculus presentation of Intuitionistic Propositional Linear Logic. The states of the register based abstract machine comprise a low-level code block, a register bank and a dump holding suspended procedure activations. Transformation of natural deduction proofs into our sequent calculus yields a type-preserving compilation function from the Linear Lambda Calculus to the abstract machine. We prove correctness of the abstract machine with respect to the standard call-by-value evaluation semantics of the Linear Lambda Calculus