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.

翻译：Accattoli、Dal Lago 和 Vanoni 近期证明了 Space KAM（Krivine抽象机的一种变体）所使用的空间，是λ演算中考虑对数空间的合理空间代价模型，解决了长期存在的开放问题。本文提出了一种新的多类型系统（交集类型的一种变体），并从多类型推导中提取 Space KAM 所使用的空间，从而将抽象机的空间复杂度捕捉到类型系统中。此外，我们通过对类型系统进行微小修改，还展示了如何捕捉 Space KAM 的时间——该时间同样是一个合理的时间代价模型。