ICFP 2024
Mon 2 - Sat 7 September 2024 Milan, Italy

This program is tentative and subject to change.

Tue 3 Sep 2024 15:48 - 16:06 - Logical Foundations

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.

This program is tentative and subject to change.

Tue 3 Sep

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

15:30 - 17:00
15:30
18m
Talk
Functional Pearl: Grokking the Sequent Calculus
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
Pre-print
15:48
18m
Talk
Call-By-Unboxed-Value
ICFP Papers and Events
Paul Downen University of Massachusetts Lowell
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, UK and University of Cambridge, UK, Cristiano Vasconcellos Santa Catarina State University
DOI Pre-print
16:42
18m
Talk
Example-Based Reasoning About the Realizability Of Polymorphic Programs
ICFP Papers and Events
Niek Mulleners Utrecht University, Johan Jeuring Utrecht University, Bastiaan Heeren Open University of the Netherlands, Netherlands
DOI Pre-print