Multi types and reasonable space
This work provides a foundational advance for theoretical computer science by formally linking type systems to space complexity analysis in lambda calculus.
The authors tackled the problem of capturing space complexity in lambda calculus by developing a new multi type system that extracts the space used by the Space KAM, solving a longstanding open problem about reasonable space cost models accounting for logarithmic space.
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.