Space-Efficient Computation by Interaction

Abstract We introduce a typed functional programming language for logarithmic space. Its type system is an annotated subsystem of Hofmann’s polytime LFPL. To guide the design of the programming language and to enable the proof of logspace -soundness, we introduce a realisability model over a variant of the Geometry of Interaction. This realisability model, which takes inspiration from Møller-Neergaard and Mairson’s work on BC \(^{\rm --}_{\epsilon}\), provides a general framework for modelling space-restricted computation.

Authors

• Ulrich Schöpp

Keywords

No keywords are indexed for this paper.