Sciweavers

Share
CSR
2008
Springer

A Semantic Proof of Polytime Soundness of Light Affine Logic

8 years 8 months ago
A Semantic Proof of Polytime Soundness of Light Affine Logic
We define a denotational 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 also is entirely semantical in nature. The model construction uses a new instance of a resource monoid; a general method for interpreting variations of linear logic with complexity restrictions introduced earlier by the authors.
Ugo Dal Lago, Martin Hofmann
Added 19 Oct 2010
Updated 19 Oct 2010
Type Conference
Year 2008
Where CSR
Authors Ugo Dal Lago, Martin Hofmann
Comments (0)
books