TY - JOUR
T1 - The Linear Logical Abstract Machine
AU - Bonelli, Eduardo
PY - 2006/5/5
Y1 - 2006/5/5
N2 - 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.
AB - 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.
KW - Abstract Machine
KW - Compilation
KW - Curry-Howard Isomorphism
KW - Linear Lambda Calculus
KW - Linear Logic
UR - http://www.scopus.com/inward/record.url?scp=33646134415&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=33646134415&partnerID=8YFLogxK
U2 - 10.1016/j.entcs.2006.04.007
DO - 10.1016/j.entcs.2006.04.007
M3 - Article
AN - SCOPUS:33646134415
SN - 1571-0661
VL - 158
SP - 99
EP - 121
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
IS - 1
ER -