The Linear Logical Abstract Machine

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....

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Bonelli, Eduardo
Formato: Articulo
Lenguaje:Inglés
Publicado: 2006
Materias:
Ciencias Informáticas
Abstract Machine
Compilation
Curry-Howard Isomorphism
Linear Lambda Calculus
Linear Logic
Acceso en línea:http://sedici.unlp.edu.ar/handle/10915/83098
Aporte de:
SEDICI (UNLP) de Universidad Nacional de La Plata
id I19-R120-10915-83098
record_format dspace
institution Universidad Nacional de La Plata
institution_str I-19
repository_str R-120
collection SEDICI (UNLP)
language Inglés
topic Ciencias Informáticas
Abstract Machine
Compilation
Curry-Howard Isomorphism
Linear Lambda Calculus
Linear Logic
spellingShingle Ciencias Informáticas
Abstract Machine
Compilation
Curry-Howard Isomorphism
Linear Lambda Calculus
Linear Logic
Bonelli, Eduardo
The Linear Logical Abstract Machine
topic_facet Ciencias Informáticas
Abstract Machine
Compilation
Curry-Howard Isomorphism
Linear Lambda Calculus
Linear Logic
description 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
format Articulo
Articulo
author Bonelli, Eduardo
author_facet Bonelli, Eduardo
author_sort Bonelli, Eduardo
title The Linear Logical Abstract Machine
title_short The Linear Logical Abstract Machine
title_full The Linear Logical Abstract Machine
title_fullStr The Linear Logical Abstract Machine
title_full_unstemmed The Linear Logical Abstract Machine
title_sort linear logical abstract machine
publishDate 2006
url http://sedici.unlp.edu.ar/handle/10915/83098
work_keys_str_mv AT bonellieduardo thelinearlogicalabstractmachine
AT bonellieduardo linearlogicalabstractmachine
bdutipo_str Repositorios
_version_ 1764820488290304003

Ejemplares similares