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.
U. Dal Lago, M. Hofmann (2010). A Semantic Proof of Polytime Soundness of Light Affine Logic. THEORY OF COMPUTING SYSTEMS, 46(4), 673-689 [10.1007/s00224-009-9210-x].
A Semantic Proof of Polytime Soundness of Light Affine Logic
DAL LAGO, UGO;
2010
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
