Sciweavers

CSL
1999
Springer
13 years 4 months ago
A P-Time Completeness Proof for Light Logics
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.
Luca Roversi
CORR
2004
Springer
123views Education» more  CORR 2004»
13 years 4 months ago
Light types for polynomial time computation in lambda-calculus
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...
Patrick Baillot, Kazushige Terui
CORR
2006
Springer
99views Education» more  CORR 2006»
13 years 4 months ago
An Embedding of the BSS Model of Computation in Light Affine Lambda-Calculus
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...
Patrick Baillot, Marco Pedicini
CSR
2008
Springer
13 years 6 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. Th...
Ugo Dal Lago, Martin Hofmann