ICFP 2024
Proceedings of the ACM on Programming Languages, Volume 8, Number ICFP
Powered by
Conference Publishing Consulting

Proceedings of the ACM on Programming Languages, Volume 8, Number ICFP, September 2–7, 2024, Milan, Italy

ICFP – Journal Issue

Contents - Abstracts - Authors

Frontmatter

Title Page
Editorial Message
Sponsors

Papers

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

proc time: 4.66