POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Thu 18 Jan 2024 09:20 - 09:40 at Turing Lecture - Higher-Order Effectful Programs Chair(s): Sam Lindley

An important aspect of building robust systems that execute on dedicated hardware and perhaps in constrained environments is to control and manage the effects performed by program code.

We present ReML, a higher-order statically-typed functional language, which allows programmers to be explicit about the effects performed by program code and in particular effects related to memory management. Allowing programmers to be explicit about effects, the regions in which values reside, and the constraints under which code execute, makes programs robust to changes in the program source code and to compiler updates, including compiler optimisations.

ReML is integrated with a polymorphic inference system that builds on top of region-inference, as it is implemented in the MLKit, a Standard ML compiler that uses region-based memory management as its primary memory management scheme.

Professor in the Programming Languages and Theory of Computation (PLTC) section at Department of Computer Science, University of Copenhagen (DIKU). Conducts research in the design and implementation of programming languages, including compilation techniques for functional languages, parallelism, memory management, and program optimisation.

Thu 18 Jan

Displayed time zone: London change

09:00 - 10:20
Higher-Order Effectful ProgramsPOPL at Turing Lecture
Chair(s): Sam Lindley University of Edinburgh
09:00
20m
Talk
On Model-Checking Higher-Order Effectful Programs
POPL
Ugo Dal Lago University of Bologna & INRIA Sophia Antipolis, Alexis Ghyselen University of Bologna
09:20
20m
Talk
Explicit Effects and Effect Constraints in ReML
POPL
Martin Elsman University of Copenhagen, Denmark
Link to publication DOI
09:40
20m
Talk
Decalf: A Directed, Effectful Cost-Aware Logical Framework
POPL
Harrison Grodin , Jonathan Sterling University of Cambridge, Yue Niu Carnegie Mellon University, Robert Harper Carnegie Mellon University
Pre-print
10:00
20m
Talk
Modular Denotational Semantics for Effects with Guarded Interaction TreesDistinguished PaperRemote
POPL
Daniel Frumin University of Groningen, Amin Timany Aarhus University, Lars Birkedal Aarhus University
DOI Pre-print