A logical account of pspace

Abstract

We propose a characterization of PSPACE by means of atype 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.