Multi types and reasonable space

TL;DR

This paper introduces a multi-type system that accurately models the space and time complexity of the Space KAM, a variant of the Krivine abstract machine, providing a type-theoretic characterization of its resource usage.

Contribution

It develops a new multi-type system that captures both space and time complexity of the Space KAM, linking type derivations to computational resource bounds.

Findings

Type system accurately models space complexity of Space KAM.

Type system also captures the time complexity with minor modifications.

Provides a type-theoretic framework for analyzing resource usage in lambda-calculus.

Abstract

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.