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.
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:
Eventuali allegati, non sono esposti
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.