Sciweavers

Share
POPL
2008
ACM

A logical account of pspace

9 years 3 months ago
A logical account of pspace
We propose a characterization of PSPACE by means of a type assignment for an extension of lambda calculus with a conditional construction. The type assignment STAB is an extension of STA, a type assignment for lambda-calculus inspired by Lafont's Soft Linear Logic. We extend STA by means of a ground type and terms for booleans. The key point is that the elimination rule for booleans is managed in an additive way. Thus, we are able to program polynomial time Alternating Turing Machines. Conversely, we introduce a call-byname evaluation machine in order to compute programs in polynomial space. As far as we know, this is the first characterization of PSPACE which is based on lambda calculus and light logics.
Marco Gaboardi, Jean-Yves Marion, Simona Ronchi De
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2008
Where POPL
Authors Marco Gaboardi, Jean-Yves Marion, Simona Ronchi Della Rocca
Comments (0)
books