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.

• Type: Conference
• Year: 2008
• Where: POPL
• Authors: Marco Gaboardi, Jean-Yves Marion, Simona Ronchi Della Rocca
• Keywords: Call-byname Evaluation Machine, POPL 2008, Programming Languages, Soft Linear Logic, Type Assignment