ICFP 2024
Mon 2 - Sat 7 September 2024 Milan, Italy
Tue 3 Sep 2024 15:48 - 16:06 at Green 1-2-3 - Logical Foundations Chair(s): Kenji Maillard

Call-By-Push-Value has famously subsumed both call-by-name and call-by-value by decomposing programs along the axis of “values” versus “computations.” Here, we introduce Call-By-Unboxed-Value which further decomposes programs along an orthogonal axis separating “atomic” versus “complex.” As the name suggests, these two dimensions make it possible to express the representations of values as boxed or unboxed, so that functions pass unboxed values as inputs and outputs. More importantly, Call-By-Unboxed-Value allows for an unrestricted mixture of polymorphism and unboxed types, giving a foundation for studying compilation techniques for polymorphism based on representation irrelevance. In this regard, we use Call-By-Unboxed-Value to formalize representation polymorphism independently of types; for the first time compiling untyped representation-polymorphic code, while nonetheless preserving types all the way to the machine.

Tue 3 Sep

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

15:30 - 17:00
Logical FoundationsICFP Papers and Events / JFP First Papers at Green 1-2-3
Chair(s): Kenji Maillard Inria
15:30
18m
Talk
Grokking the Sequent Calculus (Functional Pearl)
ICFP Papers and Events
David Binder University of Tübingen, Marco Tzschentke Universität Tübingen, Marius Müller University of Tübingen, Klaus Ostermann University of Tübingen
DOI
15:48
18m
Talk
Call-by-Unboxed-Value
ICFP Papers and Events
Paul Downen University of Massachusetts at Lowell
DOI
16:06
18m
Talk
A correct-by-construction conversion from lambda calculus to combinatory logic (JFP Functional Pearls)JFP First Paper
JFP First Papers
Wouter Swierstra Utrecht University, Netherlands
DOI
16:24
18m
Talk
On the Operational Theory of the CPS-Calculus: Towards a Theoretical Foundation for IRs
ICFP Papers and Events
Paulo Torrens University of Kent, Dominic Orchard University of Kent; University of Cambridge, Cristiano Vasconcellos Santa Catarina State University
DOI Pre-print
16:42
18m
Talk
Example-Based Reasoning about the Realizability of Polymorphic ProgramsDistinguished Paper
ICFP Papers and Events
Niek Mulleners Utrecht University, Johan Jeuring Utrecht University, Bastiaan Heeren Open Universiteit
DOI Pre-print