Sciweavers

ENTCS
2008

Soft Linear Logic and Polynomial Complexity Classes

13 years 3 months ago
Soft Linear Logic and Polynomial Complexity Classes
We describe some results inspired to Lafont's Soft Linear Logic (SLL) which is a subsystem of second-order linear logic with restricted rules for exponentials, correct and complete for polynomial time computations. SLL is the basis for the design of type assignment systems for lambda-calculus, characterizing the complexity classes PTIME, PSPACE and NPTIME. PTIME is characterized by a type assignments system where types are a proper subset of SLL formulae. The characterization consists in the fact that a well typed term can be reduced to normal form by a number of beta-reductions polynomial in its lenght, and moreover all polynomial time functions can be computed by well typed terms. PSPACE is characterized by a type assignment system obtained from the previous one, by extending the set of types by a type for booleans, and the lambda-calculus by two boolean constants and a conditional constructor. The system assigns types to terms in such a way that the evaluation of programs (clo...
Marco Gaboardi, Jean-Yves Marion, Simona Ronchi De
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Where ENTCS
Authors Marco Gaboardi, Jean-Yves Marion, Simona Ronchi Della Rocca
Comments (0)