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 Moller-Neergaard and Mairson’s work on BC$^{\rm --}_{\epsilon}$, provides a general framework for modelling space-restricted computation.