ICFP 2024 - ICFP Programming Contest

About
Program

For more information, visit https://icfpcontest2024.github.io.

Time Zone

The program is currently displayed in (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

You're viewing the program in a time zone which is different from your device's time zone change time zone

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

13:00 - 13:30	ICFP programming contest resultsICFP Programming Contest at Green 1-2-3

13:00 30m Awards		ICFP Contest Results ICFP Programming Contest

09:00 - 10:00	Tuesday keynoteICFP Papers and Events at Green 1-2-3 Chair(s): Brigitte Pientka McGill University

09:00 60m Keynote		Requirements are All You Need ICFP Papers and Events Andrew D. Gordon Cogna and University of Edinburgh Link to publication DOI File Attached

10:30 - 12:00	Algebraic and Computational EffectsICFP Papers and Events / JFP First Papers at Green 1-2-3 Chair(s): Patrick Bahr IT University of Copenhagen

10:30 18m Talk		Abstracting Effect Systems for Algebraic Effect Handlers ICFP Papers and Events Takuma Yoshioka Kyoto University, Taro Sekiyama National Institute of Informatics; SOKENDAI, Atsushi Igarashi Kyoto University DOI
10:48 18m Talk		Parallel Algebraic Effect Handlers ICFP Papers and Events Ningning Xie University of Toronto; Google DeepMind, Daniel D. Johnson University of Toronto; Google DeepMind, Dougal Maclaurin Google DeepMind, Adam Paszke Google DeepMind DOI
11:06 18m Talk		Abstract Interpreters: A Monadic Approach to Modular Verification ICFP Papers and Events Sébastien Michelland Université Grenoble-Alpes - Grenoble INP - LCIS, Yannick Zakowski Inria, Laure Gonnord Université Grenoble-Alpes - Grenoble INP - LCIS DOI Pre-print
11:24 18m Talk		Algebraic effects and handlers for arrowsJFP First Paper JFP First Papers Takahiro Sanada Fukui Prefectural University
11:42 18m Talk		How to Bake a Quantum Π ICFP Papers and Events Jacques Carette McMaster University, Chris Heunen University of Edinburgh, Robin Kaarsgaard University of Southern Denmark, Amr Sabry Indiana University DOI

13:30 - 15:00	Type TheoryICFP Papers and Events / JFP First Papers at Green 1-2-3 Chair(s): Brent Yorgey Hendrix College

13:30 18m Talk		Normalization by evaluation for modal dependent type theoryJFP First Paper JFP First Papers Jason Z.S. Hu McGill University, Junyoung Jang McGill University, Brigitte Pientka McGill University DOI
13:48 18m Talk		Closure-Free Functional Programming in a Two-Level Type Theory ICFP Papers and Events András Kovács University of Gothenburg DOI Pre-print
14:06 18m Talk		Gradual Indexed Inductive Types ICFP Papers and Events Mara Malewski Correa University of Chile, Kenji Maillard Inria, Nicolas Tabareau Inria, Éric Tanter University of Chile DOI
14:24 18m Talk		Dependent Ghosts Have a Reflection for Free ICFP Papers and Events Théo Winterhalter Inria DOI
14:42 18m Talk		Static Blame for gradual typingJFP First Paper JFP First Papers Chenghao Su Nanjing University, Lin Chen Nanjing University, Yanhui Li Nanjing University, Yuming Zhou Nanjing University DOI

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

09:00 - 10:00	Wednesday keynoteICFP Papers and Events at Green 1-2-3 Chair(s): Andrew Kennedy Facebook London

09:00 60m Keynote		Capabilities for Control ICFP Papers and Events Martin Odersky EPFL

ICFP Programming Contest

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

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

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

Tracks

Workshops

Co-hosted Symposia

	17:00 - 17:15	Introduction of Industrial SponsorsICFP Papers and Events at Green 1-2-3

	17:15 - 18:15	Memorial for D. Turner & ArvindICFP Papers and Events at Green 1-2-3 Chair(s): Marco Gaboardi Boston University

10:30 - 12:00	Meta-Programming, Staging, Generic Programming, Partial EvaluationICFP Papers and Events / JFP First Papers at Green 1-2-3 Chair(s): Richard A. Eisenberg Jane Street

10:30 18m Talk		Staged Compilation with Module Functors ICFP Papers and Events Tsung-Ju Chiang University of Toronto, Jeremy Yallop University of Cambridge, Leo White Jane Street, Ningning Xie University of Toronto; Google DeepMind DOI Pre-print
10:48 18m Talk		A Safe Low-Level Language for Computer Algebra and Its Formally Verified Compiler ICFP Papers and Events Guillaume Melquiond Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria, Josué Moreau Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria DOI
11:06 18m Talk		Deriving with Derivatives: Optimizing Incremental Fixpoints for Higher-Order Flow Analysis ICFP Papers and Events Benjamin Quiring University of Maryland at College Park, David Van Horn University of Maryland DOI
11:24 18m Talk		Compiled, Extensible, Multi-language DSLs (Functional Pearl)Functional Pearl ICFP Papers and Events Michael Ballantyne Northeastern University, Mitch Gamburg Unaffiliated, Jason Hemann Seton Hall University DOI Pre-print
11:42 18m Talk		Knuth–Morris–Pratt illustrated (JFP Functional Pearls )JFP First Paper JFP First Papers Cameron Moy Northeastern University DOI

13:30 - 15:00	Separation Logic ICFP Papers and Events at Green 1-2-3 Chair(s): Jacques Garrigue Nagoya University

13:30 18m Talk		Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic ProgramsDistinguished Paper ICFP Papers and Events Alejandro Aguirre Aarhus University, Philipp G. Haselwarter Aarhus University, Markus de Medeiros New York University, Kwing Hei Li Aarhus University, Simon Oddershede Gregersen New York University, Joseph Tassarotti New York University, Lars Birkedal Aarhus University DOI Pre-print
13:48 18m Talk		Snapshottable StoresDistinguished Paper ICFP Papers and Events Clément Allain Inria, Basile Clément OCamlPro, Alexandre Moine Inria, Gabriel Scherer Université Paris Cité - Inria - CNRS DOI
14:06 18m Talk		Almost-Sure Termination by Guarded Refinement ICFP Papers and Events Simon Oddershede Gregersen New York University, Alejandro Aguirre Aarhus University, Philipp G. Haselwarter Aarhus University, Joseph Tassarotti New York University, Lars Birkedal Aarhus University DOI Pre-print
14:24 18m Talk		Refinement Composition Logic ICFP Papers and Events Youngju Song MPI-SWS, Dongjae Lee Seoul National University DOI
14:42 18m Talk		Specification and Verification for Unrestricted Algebraic Effects and Handling ICFP Papers and Events Yahui Song National University of Singapore, Darius Foo National University of Singapore, Wei-Ngan Chin National University of Singapore DOI Pre-print

15:30 - 16:42	Verification and Cost AnalysisJFP First Papers / ICFP Papers and Events at Green 1-2-3 Chair(s): Clément Pit-Claudel EPFL

15:30 18m Talk		Story of Your Lazy Function’s Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy Programs ICFP Papers and Events Li-yao Xia Unaffiliated, Laura Israel Portland State University, Maite Kramarz University of Toronto, Nicholas Coltharp Portland State University, Koen Claessen Chalmers University of Technology, Stephanie Weirich University of Pennsylvania, Yao Li Portland State University DOI Pre-print
15:48 18m Talk		Level-p-complexity of Boolean functions using thinning, memoization, and polynomialsJFP First Paper JFP First Papers Julia Jansson , Patrik Jansson Chalmers University of Technology and University of Gothenbrug DOI
16:06 18m Talk		CCLemma: E-Graph Guided Lemma Discovery for Inductive Equational Proofs ICFP Papers and Events Cole Kurashige University of California at San Diego, Ruyi Ji Peking University, Aditya Giridharan University of California at San Diego, Mark Barbone University of California at San Diego, Daniel Noor Technion, Shachar Itzhaky Technion, Ranjit Jhala University of California at San Diego, Nadia Polikarpova University of California at San Diego DOI
16:24 18m Talk		Contract Lenses: Reasoning about Bidirectional Programs via CalculationJFP First Paper JFP First Papers Hanliang Zhang University of Bristol, UK, Wenhao Tang University of Edinburgh, Ruifeng Xie Peking University, Meng Wang University of Bristol, Zhenjiang Hu Peking University DOI

17:15 - 18:30	Business MeetingICFP Papers and Events at Green 1-2-3 Chair(s): Marco Gaboardi Boston University

17:15 15m Other		Remembering Alan Jeffrey ICFP Papers and Events
17:30 5m Awards		ICFP 2014 Most Influential Paper Award ICFP Papers and Events Marco Gaboardi Boston University
17:35 5m Awards		Recognition of Distinguished Papers ICFP Papers and Events Brigitte Pientka McGill University
17:40 5m Talk		SRC Awards ICFP Papers and Events Kuen-Bang Hou (Favonia) University of Minnesota, J. Garrett Morris University of Iowa
17:45 10m Other		The functioning of ICFP ICFP Papers and Events Sam Lindley University of Edinburgh File Attached
17:55 5m Talk		Diversity, equality, and inclusion at ICFP ICFP Papers and Events Alejandro Russo Chalmers University of Technology, Sweden / University of Gothenburg, Sweden / DPella AB, Sweden
18:00 10m Other		General Chair report ICFP Papers and Events Marco Gaboardi Boston University
18:10 15m Other		PC Chair's report ICFP Papers and Events Brigitte Pientka McGill University
18:25 5m Other		ICFP 2025 announcement ICFP Papers and Events Ilya Sergey National University of Singapore

09:00 - 10:00	Thursday keynoteICFP Papers and Events at Green 1-2-3 Chair(s): Neel Krishnaswami University of Cambridge

09:00 60m Keynote		Refinement Types from Light to Deep Verification ICFP Papers and Events Niki Vazou IMDEA Software Institute

10:30 - 12:00	Refinement Types, Type InferenceICFP Papers and Events / JFP First Papers at Green 1-2-3 Chair(s): Dominic Orchard University of Kent; University of Cambridge

10:30 18m Talk		The Long Way to Deforestation: A Type Inference and Elaboration Technique for Removing Intermediate Data StructuresDistinguished Paper ICFP Papers and Events Yijia Chen Hong Kong University of Science and Technology, Lionel Parreaux HKUST (The Hong Kong University of Science and Technology) DOI
10:48 18m Talk		Contextual Typing ICFP Papers and Events Xu Xue University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong DOI
11:06 18m Talk		Synchronous Programming with Refinement Types ICFP Papers and Events Jiawei Chen University of Michigan at Ann Arbor, José Luiz Vargas de Mendonça University of Michigan at Ann Arbor, Bereket Shimels Ayele Addis Ababa Institute of Technology, Bereket Ngussie Bekele Addis Ababa Institute of Technology, Shayan Jalili University of Michigan at Ann Arbor, Pranjal Sharma University of Michigan at Ann Arbor, Nicholas Wohlfeil University of Michigan at Ann Arbor, Yicheng Zhang University of Michigan at Ann Arbor, Jean-Baptiste Jeannin University of Michigan at Ann Arbor DOI
11:24 18m Talk		Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System ICFP Papers and Events Satoshi Kura Waseda University, Hiroshi Unno Tohoku University DOI File Attached
11:42 18m Talk		Trace contractsJFP First Paper JFP First Papers Cameron Moy Northeastern University, Matthias Felleisen Northeastern University DOI

13:30 - 15:00	Memory Models / Memory Management / Low-Level LanguagesICFP Papers and Events at Green 1-2-3 Chair(s): Stefan Monnier Université de Montréal

13:30 18m Talk		Oxidizing OCaml with Modal Memory Management ICFP Papers and Events Anton Lorenzen University of Edinburgh, Leo White Jane Street, Stephen Dolan Jane Street, Richard A. Eisenberg Jane Street, Sam Lindley University of Edinburgh DOI Pre-print
13:48 18m Talk		A Two-Phase Infinite/Finite Low-Level Memory Model: Reconciling Integer–Pointer Casts, Finite Space, and undef at the LLVM IR Level of Abstraction ICFP Papers and Events Calvin Beck University of Pennsylvania, Irene Yoon Inria, Hanxi Chen University of Pennsylvania, Yannick Zakowski Inria, Steve Zdancewic University of Pennsylvania DOI
14:06 18m Talk		Double-Ended Bit-Stealing for Algebraic Data Types ICFP Papers and Events Martin Elsman University of Copenhagen Link to publication DOI
14:24 18m Talk		Beyond Trees: Calculating Graph-Based Compilers (Functional Pearl)Functional Pearl ICFP Papers and Events Patrick Bahr IT University of Copenhagen, Graham Hutton University of Nottingham DOI Pre-print
14:42 18m Talk		Sound Borrow-Checking for Rust via Symbolic Semantics ICFP Papers and Events Son Ho Inria, Aymeric Fromherz Inria, Jonathan Protzenko Microsoft Azure Research DOI

15:30 - 17:00	Distributed Systems, ConcurrencyICFP Papers and Events / JFP First Papers at Green 1-2-3 Chair(s): Michael Sperber Active Group GmbH

15:30 18m Talk		The Functional, the Imperative, and the Sudoku: Getting Good, Bad, and Ugly to Get Along (Functional Pearl)Functional Pearl ICFP Papers and Events Manuel Serrano Inria; Université Côte d’Azur, Robert Bruce Findler Northwestern University DOI
15:48 18m Talk		Blame-Correct Support for Receiver Properties in Recursively-Structured Actor Contracts ICFP Papers and Events Bram Vandenbogaerde Vrije Universiteit Brussel, Quentin Stiévenart Université du Québec à Montréal, Coen De Roover Vrije Universiteit Brussel DOI Pre-print
16:06 18m Talk		A Coq Mechanization of JavaScript Regular Expression Semantics ICFP Papers and Events Noé De Santo EPFL, Aurèle Barrière EPFL, Clément Pit-Claudel EPFL Link to publication DOI Pre-print
16:24 18m Talk		Alice or Bob?: Process polymorphism in choreographiesJFP First Paper JFP First Papers Eva Graversen University of Southern Denmark, Andrew K. Hirsch University at Buffalo, SUNY, Fabrizio Montesi University of Southern Denmark DOI
16:42 18m Talk		Functional Programming in Financial Markets (Experience Report)Experience Report ICFP Papers and Events Atze Dijkstra Standard Chartered Bank, José Pedro Magalhães Standard Chartered Bank, Pierre Néron Standard Chartered Bank DOI Pre-print

	12:00 - 13:30	LunchCatering at Catering Area

ICFP Programming Contest

Program Display Configuration

Tue 3 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Wed 4 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Thu 5 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

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

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

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