A type system for PSPACE derived from light linear logic
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 build DLALB we start from DLAL (which has a simple type language with a linear and an intuitionistic type arrow, as well a...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2012-01-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1201.1122v1 |