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

The sequent calculus is a proof system which was designed as a more symmetric alternative to natural deduction. The 𝜆𝜇𝜇-calculus is a term assignment system for the sequent calculus and a great foundation for compiler intermediate languages due to its first-class representation of evaluation contexts. Unfortunately, only experts of the sequent calculus can appreciate its beauty. To remedy this, we present the first introduction to the 𝜆𝜇𝜇-calculus which is not directed at type theorists or logicians but at compiler hackers and programming-language enthusiasts. We do this by writing a compiler from a small but interesting surface language to the 𝜆𝜇𝜇-calculus as a compiler intermediate language.

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