Treffer: Author manuscript, published in 'Symposium on Principles of Programming Languages- POPL'08, San Francisco: États-Unis d'Amérique (2008)' A Logical account of PSPACE
Title:
Author manuscript, published in 'Symposium on Principles of Programming Languages- POPL'08, San Francisco: États-Unis d'Amérique (2008)' A Logical account of PSPACE
Authors:
Contributors:
The Pennsylvania State University CiteSeerX Archives
Publication Year:
2008
Collection:
CiteSeerX
Document Type:
Fachzeitschrift
text
File Description:
application/pdf
Language:
English
Availability:
Rights:
Metadata may be used without restrictions as long as the oai identifier remains attached to it.
Accession Number:
edsbas.75EFF1CB
Database:
BASE
Weitere Informationen
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. 1.