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....
Guardado en:
Autor principal: | |
---|---|
Formato: | Articulo |
Lenguaje: | Inglés |
Publicado: |
2006
|
Materias: | |
Acceso en línea: | http://sedici.unlp.edu.ar/handle/10915/83098 |
Aporte de: |
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 |