ICFP 2024
Proceedings of the ACM on Programming Languages, Volume 8, Number ICFP

Title Page

Editorial Message

Sponsors

How to Bake a Quantum Π
Jacques Carette, Chris Heunen, Robin Kaarsgaard, and Amr Sabry
(McMaster University, Canada; University of Edinburgh, United Kingdom; University of Southern Denmark, Denmark; Indiana University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Story of Your Lazy Function’s Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy Programs
Li-yao Xia, Laura Israel, Maite Kramarz, Nicholas Coltharp, Koen Claessen, Stephanie Weirich, and Yao Li
(Unaffiliated, France; Portland State University, USA; University of Toronto, Canada; Chalmers University of Technology, Sweden; University of Pennsylvania, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Compiled, Extensible, Multi-language DSLs (Functional Pearl)
Michael Ballantyne, Mitch Gamburg, and Jason Hemann
(Northeastern University, USA; Unaffiliated, USA; Seton Hall University, USA)

Publisher's Version

Double-Ended Bit-Stealing for Algebraic Data Types
Martin Elsman
(University of Copenhagen, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

A Safe Low-Level Language for Computer Algebra and Its Formally Verified Compiler
Guillaume Melquiond and Josué Moreau
(Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

On the Operational Theory of the CPS-Calculus: Towards a Theoretical Foundation for IRs
Paulo Torrens, Dominic Orchard, and Cristiano Vasconcellos
(University of Kent, United Kingdom; University of Cambridge, United Kingdom; Santa Catarina State University, Brazil)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

The Functional, the Imperative, and the Sudoku: Getting Good, Bad, and Ugly to Get Along (Functional Pearl)
Manuel Serrano and Robert Bruce Findler
(Inria, France; Université Côte d’Azur, France; Northwestern University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Almost-Sure Termination by Guarded Refinement
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, and Lars Birkedal
(New York University, USA; Aarhus University, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Functional Programming in Financial Markets (Experience Report)
Atze Dijkstra, José Pedro Magalhães, and Pierre Néron
(Standard Chartered Bank, United Kingdom; Standard Chartered Bank, Singapore)

Publisher's Version

The Long Way to Deforestation: A Type Inference and Elaboration Technique for Removing Intermediate Data Structures
Yijia Chen and Lionel Parreaux
(Hong Kong University of Science and Technology, Hong Kong, China)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Functional

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, and Lars Birkedal
(Aarhus University, Denmark; New York University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Example-Based Reasoning about the Realizability of Polymorphic Programs
Niek Mulleners, Johan Jeuring, and Bastiaan Heeren
(Utrecht University, Netherlands; Open Universiteit, Netherlands)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Snapshottable Stores
Clément Allain, Basile Clément, Alexandre Moine, and Gabriel Scherer
(Inria, France; OCamlPro, France; Université Paris Cité - Inria - CNRS, France)

Publisher's Version

Beyond Trees: Calculating Graph-Based Compilers (Functional Pearl)
Patrick Bahr and Graham Hutton
(IT University of Copenhagen, Denmark; University of Nottingham, United Kingdom)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Grokking the Sequent Calculus (Functional Pearl)
David Binder, Marco Tzschentke, Marius Müller, and Klaus Ostermann
(University of Tübingen, Germany)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable

Sound Borrow-Checking for Rust via Symbolic Semantics
Son Ho, Aymeric Fromherz, and Jonathan Protzenko
(Inria, France; Microsoft Azure Research, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Abstracting Effect Systems for Algebraic Effect Handlers
Takuma Yoshioka, Taro Sekiyama, and Atsushi Igarashi
(Kyoto University, Japan; National Institute of Informatics, Japan; SOKENDAI, Japan)

Publisher's Version Archive submitted (740 kB)

Oxidizing OCaml with Modal Memory Management
Anton Lorenzen, Leo White, Stephen Dolan, Richard A. Eisenberg, and Sam Lindley
(University of Edinburgh, United Kingdom; Jane Street, United Kingdom; Jane Street, USA)

Publisher's Version Archive submitted (890 kB)

Blame-Correct Support for Receiver Properties in Recursively-Structured Actor Contracts
Bram Vandenbogaerde, Quentin Stiévenart, and Coen De Roover
(Vrije Universiteit Brussel, Belgium; Université du Québec à Montréal, Canada)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Gradual Indexed Inductive Types
Mara Malewski, Kenji Maillard, Nicolas Tabareau, and Éric Tanter
(University of Chile, Chile; Inria, France)

Publisher's Version

Refinement Composition Logic
Youngju Song and Dongjae Lee
(MPI-SWS, Germany; Seoul National University, South Korea)

Publisher's Version

Abstract Interpreters: A Monadic Approach to Modular Verification
Sébastien Michelland, Yannick Zakowski, and Laure Gonnord
(Université Grenoble-Alpes - Grenoble INP - LCIS, France; Inria - ENS de Lyon - CNRS - UCBL1 - LIP - UMR 5668, France)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable

Dependent Ghosts Have a Reflection for Free
Théo Winterhalter
(Inria, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Closure-Free Functional Programming in a Two-Level Type Theory
András Kovács
(University of Gothenburg, Sweden)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Staged Compilation with Module Functors
Tsung-Ju Chiang, Jeremy Yallop, Leo White, and Ningning Xie
(University of Toronto, Canada; University of Cambridge, United Kingdom; Jane Street, United Kingdom)

Publisher's Version

Deriving with Derivatives: Optimizing Incremental Fixpoints for Higher-Order Flow Analysis
Benjamin Quiring and David Van Horn
(University of Maryland at College Park, USA; University of Maryland, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Parallel Algebraic Effect Handlers
Ningning Xie, Daniel D. Johnson, Dougal Maclaurin, and Adam Paszke
(University of Toronto, Canada; Google DeepMind, Canada; Google DeepMind, USA; Google DeepMind, Germany)

Publisher's Version

A Two-Phase Infinite/Finite Low-Level Memory Model: Reconciling Integer–Pointer Casts, Finite Space, and undef at the LLVM IR Level of Abstraction
Calvin Beck, Irene Yoon, Hanxi Chen, Yannick Zakowski, and Steve Zdancewic
(University of Pennsylvania, USA; Inria, France; Inria - ENS de Lyon - CNRS - UCBL1 - LIP - UMR 5668, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

CCLemma: E-Graph Guided Lemma Discovery for Inductive Equational Proofs
Cole Kurashige, Ruyi Ji, Aditya Giridharan, Mark Barbone, Daniel Noor, Shachar Itzhaky, Ranjit Jhala, and Nadia Polikarpova
(University of California at San Diego, USA; Peking University, China; Technion, Israel)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Call-by-Unboxed-Value
Paul Downen
(University of Massachusetts at Lowell, USA)

Publisher's Version

Contextual Typing
Xu Xue and Bruno C. d. S. Oliveira
(University of Hong Kong, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Specification and Verification for Unrestricted Algebraic Effects and Handling
Yahui Song, Darius Foo, and Wei-Ngan Chin
(National University of Singapore, Singapore)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Synchronous Programming with Refinement Types
Jiawei Chen, José Luiz Vargas de Mendonça, Bereket Shimels Ayele, Bereket Ngussie Bekele, Shayan Jalili, Pranjal Sharma, Nicholas Wohlfeil, Yicheng Zhang, and Jean-Baptiste Jeannin
(University of Michigan at Ann Arbor, USA; Addis Ababa Institute of Technology, Ethiopia)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System
Satoshi Kura and Hiroshi Unno
(Waseda University, Japan; Tohoku University, Japan)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

A Coq Mechanization of JavaScript Regular Expression Semantics
Noé De Santo, Aurèle Barrière, and Clément Pit-Claudel
(EPFL, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable