We explain why the original proofs of P-Time completeness for Light Affine Logic and Light Linear Logic can not work, and we fully develop a working one.
We present a polymorphic type system for lambda calculus ensuring that welltyped programs can be executed in polynomial time: dual light affine logic (DLAL). DLAL has a simple typ...
This paper brings together two lines of research: implicit characterization of complexity classes by Linear Logic (LL) on the one hand, and computation over an arbitrary ring in t...
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. Th...