The Linear Logical Abstract Machine

Research output: Contribution to journalArticlepeer-review

1 Scopus citations

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.

Original languageEnglish
Pages (from-to)99-121
Number of pages23
JournalElectronic Notes in Theoretical Computer Science
Volume158
Issue number1
DOIs
StatePublished - 5 May 2006

Keywords

  • Abstract Machine
  • Compilation
  • Curry-Howard Isomorphism
  • Linear Lambda Calculus
  • Linear Logic

Fingerprint

Dive into the research topics of 'The Linear Logical Abstract Machine'. Together they form a unique fingerprint.

Cite this