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

The denotational semantics of the untyped $\lambda$-calculus is a well developed field built around the concept of solvable terms, which are elegantly characterized in many different ways. In particular, unsolvable terms provide a consistent notion of meaningless term. The semantics of the untyped \textit{call-by-value} $\lambda$-calculus is instead still in its infancy, because of some inherent difficulties but also because call-by-value solvable terms are less studied and understood than in call-by-name. On the one hand, we show that a carefully crafted presentation of call-by-value allows us to recover many of the properties that solvability has in call-by-name, in particular qualitative and quantitative characterizations via multi types. On the other hand, we stress that, in call-by-value, solvability plays a different role: identifying unsolvable terms as meaningless induces an inconsistent theory.

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