Sciweavers

CSL
1999
Springer
13 years 10 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 10 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 11 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
14 years 22 days 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