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 λ-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.

@article{paperbot1503,
  title = {Multi types and reasonable space},
  author = {Beniamino Accattoli and Ugo Dal Lago and Gabriele Vanoni},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {6},
  number = {ICFP},
  year = {2022},
  doi = {10.1145/3547650}
}