loading...
Light Logics and Optimal Reduction: Completeness and Complexity
Wroclaw, Poland July 10-July 14
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2007.2722nd Annual IEEE Symposium on Logic i ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Patrick Baillot, LIPN, CNRS & Universite Paris Nord, France
Paolo Coppola, Universita di Udine, Italy
Ugo Dal Lago, Universita di Bologna, Italy
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 simple geometry of interaction model (context semantics).
Citation:
Patrick Baillot, Paolo Coppola, Ugo Dal Lago, "Light Logics and Optimal Reduction: Completeness and Complexity," lics, pp.421-430, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), 2007
Usage of this product signifies your acceptance of the Terms of Use.