Sciweavers

Share
FSTTCS
2005
Springer

Quantitative Models and Implicit Complexity

10 years 16 days ago
Quantitative Models and Implicit Complexity
We give new proofs of soundness (all representable functions on base types lies in certain complexity classes) for Light Affine Logic, Elementary Affine Logic, LFPL and Soft Affine Logic. The proofs are based on a common semantical framework which is merely instantiated in four different ways. The framework consists of an innovative modification of realizability which allows us to use resource-bounded computations as realisers as opposed to including all Turing computable functions as is usually the case in realizability constructions. For example, all realisers in the model for LFPL are polynomially bounded computations whence soundness holds by construction of the model. The work then lies in being able to interpret all the required constructs in the model. While being the first entirely semantical proof of polytime soundness for light logics, our proof also provides a notable simplification of the original already semantical proof of polytime soundness for LFPL. A new result ...
Ugo Dal Lago, Martin Hofmann
Added 27 Jun 2010
Updated 27 Jun 2010
Type Conference
Year 2005
Where FSTTCS
Authors Ugo Dal Lago, Martin Hofmann
Comments (0)
books