Typing of lambda-terms in Elementary and Light Affine Logic (EAL, LAL resp.) has been studied for two different reasons: on the one hand the evaluation of typed terms using LAL (EAL, resp.) proof-nets admits a guaranteed polynomial (elementary, resp.) bound; on the other hand these terms can also be evaluated by optimal reduction using the abstract version of Lamping's algorithm. The first reduction is global while the second one is local and asynchronous. We prove that for LAL (EAL resp.) typed terms, Lamping's abstract algorithm also admits a polynomial (elementary, resp.) bound. We also show its soundness and completeness (for EAL and LAL with type fixpoints), by using a simply geometry of interaction model (contexts semantics).

P. Baillot, P. Coppola, U. Dal Lago (2007). Light Logics and Optimal Reduction: Completeness and Complexity. s.l : s.m..

Light Logics and Optimal Reduction: Completeness and Complexity

DAL LAGO, UGO
2007

Abstract

Typing of lambda-terms in Elementary and Light Affine Logic (EAL, LAL resp.) has been studied for two different reasons: on the one hand the evaluation of typed terms using LAL (EAL, resp.) proof-nets admits a guaranteed polynomial (elementary, resp.) bound; on the other hand these terms can also be evaluated by optimal reduction using the abstract version of Lamping's algorithm. The first reduction is global while the second one is local and asynchronous. We prove that for LAL (EAL resp.) typed terms, Lamping's abstract algorithm also admits a polynomial (elementary, resp.) bound. We also show its soundness and completeness (for EAL and LAL with type fixpoints), by using a simply geometry of interaction model (contexts semantics).
2007
Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science (LICS '07)
421
430
P. Baillot, P. Coppola, U. Dal Lago (2007). Light Logics and Optimal Reduction: Completeness and Complexity. s.l : s.m..
P. Baillot; P. Coppola; U. Dal Lago
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/60340
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 4
  • ???jsp.display-item.citation.isi??? 5
social impact