A Semantic Proof of Polytime Soundness of Light Affine Logic

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.