The Linear Logical Abstract Machine

EDUARDO BONELLI

Electronic Notes in Theoretical Computer Science

Elsevier Science

Año: 2006 vol. 158 p. 99 - 121

1571-0661

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.