Multi types and reasonable space
Abstract
Accattoli, Dal Lago, and Vanoni have recently proved that the space used by the Space KAM, a variant of the Krivine abstract machine, is a reasonable space cost model for the lambda-calculus accounting for logarithmic space, solving a longstanding open problem. In this paper, we provide a new system of multi types (a variant of intersection types) and extract from multi type derivations the space used by the Space KAM, capturing into a type system the space complexity of the abstract machine. Additionally, we show how to capture also the time of the Space KAM, which is a reasonable time cost model, via minor changes to the type system.
Fields of Study & Subjects
Logic
programming
and type systems
semigroups and automata theory
Computability
AI Algorithms
Publication details
- Journal / source
- Journal of Functional Programming
- Publisher
- Centre pour la Communication Scientifique Directe (CCSD)
- Volume
- Volume 36
- Publication date
- 14 August 2026
- Language
- EN