ICFP 2022
Sun 11 - Fri 16 September 2022 Ljubljana, Slovenia
Mon 12 Sep 2022 11:30 - 11:50 at Linhart - Lambda Calculus and Semantics Chair(s): Silvia Ghilezan

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 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
20m
Talk
The Theory of Call-by-Value Solvability
ICFP Papers and Events
Beniamino Accattoli Inria & Ecole Polytechnique, Giulio Guerrieri Huawei Edinburgh Research Centre
DOI
10:50
20m
Talk
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
20m
Talk
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
20m
Talk
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
20m
Talk
Denotational semantics as a foundation for cost recurrence extraction for functional languagesJFP Presentation
ICFP Papers and Events
Norman Danner Wesleyan University, Daniel R. Licata Wesleyan University