A type system for PSPACE derived from light linear logic

Lucien Capedevielle

We present a polymorphic type system for lambda calculus ensuring that well-typed programs can be executed in polynomial space: dual light affine logic with booleans (DLALB). To bu…