论文标题
多类型和合理的空间（长版）
Multi Types and Reasonable Space (Long Version)
论文作者
论文摘要
Accattoli，Dal Lago和Vanoni最近证明，Krivine Abstrack Machine的空间KAM使用的空间是Lambda-Calculus的合理空间成本模型，该模型核算对数空间，解决了一个长期存在的开放问题。在本文中，我们提供了一个新的多类型系统（相交类型的变体），并从多类型派生中提取空间KAM使用的空间，捕获到类型的系统中，抽象机的空间复杂性。此外，我们还展示了如何通过对类型系统的较小更改来捕获空间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 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.
