Accattoli, Dal Lago, and Vanoni have recently proved that the space used by the \textit{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 \textit{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.
Mon 12 SepDisplayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change
Mon 12 Sep
Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change
10:30 - 12:10 | Lambda Calculus and SemanticsICFP Papers and Events at Linhart Chair(s): Silvia Ghilezan University of Novi Sad, Mathematical Institute SASA | ||
10:30 20mTalk | The Theory of Call-by-Value Solvability ICFP Papers and Events DOI | ||
10:50 20mTalk | A Simple and Efficient Implementation of Strong Call by Need by an Abstract Machine ICFP Papers and Events Malgorzata Biernacka University of Wrocław, Witold Charatonik University of Wrocław, Faculty of Mathematics and Computer Science, Tomasz Drab University of Wrocław, Faculty of Mathematics and Computer Science DOI | ||
11:10 20mTalk | On Feller Continuity and Full Abstraction ICFP Papers and Events Gilles Barthe MPI-SP, Germany / IMDEA Software Institute, Spain, Raphaëlle Crubillé CNRS, Ugo Dal Lago University of Bologna; Inria, Francesco Gavazzo University of Bologna & INRIA Sophia Antipolis DOI | ||
11:30 20mTalk | Multi Types and Reasonable SpaceDistinguished Paper ICFP Papers and Events Beniamino Accattoli Inria & Ecole Polytechnique, Ugo Dal Lago University of Bologna; Inria, Gabriele Vanoni University of Bologna & INRIA Sophia Antipolis DOI | ||
11:50 20mTalk | Denotational semantics as a foundation for cost recurrence extraction for functional languagesJFP Presentation ICFP Papers and Events |