CRIS Current Research Information System
IRIS è la soluzione IT che facilita la raccolta e la gestione dei dati relativi alle attività e ai prodotti della ricerca. Fornisce a ricercatori, amministratori e valutatori gli strumenti per monitorare i risultati della ricerca, aumentarne la visibilità e allocare in modo efficace le risorse disponibili.
EnglishWe define realizability semantics for Light Affine Logic (LAL) which has the property that denotations of functions are polynomial time computable by construction of the model. This gives a new proof of polytime-soundness of LAL which is considerably simpler than the standard proof based on proof nets and is entirely semantical in nature. The model construction uses a new instance of a resource monoid, a general method for interpreting systems based on Linear Logic introduced earlier by the authors.
| Titolo: | A Semantic Proof of Polytime Soundness of Light Affine Logic |
| Autore/i: | DAL LAGO, UGO; M. Hofmann |
| Autore/i Unibo: | |
| Anno: | 2010 |
| Rivista: | |
| Digital Object Identifier (DOI): | http://dx.doi.org/10.1007/s00224-009-9210-x |
| Abstract: | We define realizability semantics for Light Affine Logic (LAL) which has the property that denotations of functions are polynomial time computable by construction of the model. This gives a new proof of polytime-soundness of LAL which is considerably simpler than the standard proof based on proof nets and is entirely semantical in nature. The model construction uses a new instance of a resource monoid, a general method for interpreting systems based on Linear Logic introduced earlier by the authors. |
| Data prodotto definitivo in UGOV: | 2011-02-22 17:32:40 |
| Appare nelle tipologie: | 1.01 Articolo in rivista |
File in questo prodotto:
http://hdl.handle.net/11585/99254
Copyright © 2021