一句话：提出多重类型系统，从类型推导中抽取 Space KAM 的空间开销，并捕获其合理空间与时间成本模型。
本文研究如何用类型系统刻画 λ-演算抽象机器的复杂度。此前 Accattoli 等人已证明 Krivine 抽象机变体 Space KAM 的空间是合理空间成本模型，并可刻画对数空间，但尚未由类型系统捕获。作者提出一种新的多重类型系统（交集类型变体），从多重类型推导中抽取 Space KAM 所使用的空间，从而把该抽象机的空间复杂度内化到类型系统中。作者还通过少量修改，使类型系统同样捕获 Space KAM 的时间，而该时间已是合理时间成本模型。结果给出 Space KAM 空间与时间的类型论刻画。
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}
}