The Linear Logical Abstract Machine

dc.creatorBonelli, Eduardo
dc.date2006
dc.date2019-10-10T17:51:35Z
dc.identifierhttp://sedici.unlp.edu.ar/handle/10915/83098
dc.identifierissn:1571-0661
dc.descriptionWe 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
dc.descriptionLaboratorio de Investigación y Formación en Informática Avanzada
dc.formatapplication/pdf
dc.format99-121
dc.languageen
dc.rightshttp://creativecommons.org/licenses/by-nc-sa/4.0/
dc.rightsCreative Commons Attribution-NonCommercial-ShareAlike 4.0 International (CC BY-NC-SA 4.0)
dc.subjectCiencias Informáticas
dc.subjectAbstract Machine
dc.subjectCompilation
dc.subjectCurry-Howard Isomorphism
dc.subjectLinear Lambda Calculus
dc.subjectLinear Logic
dc.titleThe Linear Logical Abstract Machine
dc.typeArticulo
dc.typeArticulo


Este ítem pertenece a la siguiente institución