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 ORCID logo, Chris Heunen ORCID logo, Robin Kaarsgaard ORCID logo, and Amr Sabry ORCID logo
(McMaster University, Canada; University of Edinburgh, United Kingdom; University of Southern Denmark, Denmark; Indiana University, USA)
Article Search 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 ORCID logo, Laura Israel ORCID logo, Maite Kramarz ORCID logo, Nicholas Coltharp ORCID logo, Koen Claessen ORCID logo, Stephanie Weirich ORCID logo, and Yao LiORCID logo
(Unaffiliated, France; Portland State University, USA; University of Toronto, Canada; Chalmers University of Technology, Sweden; University of Pennsylvania, USA)
Preprint Artifacts Available Artifacts Functional
Compiled, Extensible, Multi-language DSLs (Functional Pearl)
Michael Ballantyne ORCID logo, Mitch Gamburg ORCID logo, and Jason Hemann ORCID logo
(Northeastern University, USA; Unaffiliated, USA; Seton Hall University, USA)
Article Search
Double-Ended Bit-Stealing for Algebraic Data Types
Martin Elsman ORCID logo
(University of Copenhagen, Denmark)
Article Search Artifacts Available Artifacts Reusable
A Safe Low-Level Language for Computer Algebra and Its Formally Verified Compiler
Guillaume Melquiond ORCID logo and Josué Moreau ORCID logo
(Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria - LMF, France)
Article Search Artifacts Available Artifacts Reusable
On the Operational Theory of the CPS-Calculus: Towards a Theoretical Foundation for IRs
Paulo Torrens ORCID logo, Dominic Orchard ORCID logo, and Cristiano Vasconcellos ORCID logo
(University of Kent, United Kingdom; University of Cambridge, United Kingdom; Santa Catarina State University, Brazil)
Article Search Artifacts Available Artifacts Functional
The Functional, the Imperative, and the Sudoku: Making Good, Bad, and Ugly More Than the Sum of Their Parts (Functional Pearl)
Manuel SerranoORCID logo and Robert Bruce Findler ORCID logo
(Inria, France; Université Côte d’Azur, France; Northwestern University, USA)
Article Search Artifacts Available Artifacts Reusable
Almost-Sure Termination by Guarded Refinement
Simon Oddershede Gregersen ORCID logo, Alejandro Aguirre ORCID logo, Philipp G. Haselwarter ORCID logo, Joseph Tassarotti ORCID logo, and Lars BirkedalORCID logo
(New York University, USA; Aarhus University, Denmark)
Preprint Artifacts Available Artifacts Reusable
Functional Programming in Financial Markets (Experience Report)
Atze Dijkstra ORCID logo, José Pedro Magalhães ORCID logo, and Pierre Néron ORCID logo
(Standard Chartered Bank, United Kingdom; Standard Chartered Bank, Singapore)
Article Search
The Long Way to Deforestation: A Type Inference and Elaboration Technique for Removing Intermediate Data Structures
Yijia Chen ORCID logo and Lionel Parreaux ORCID logo
(Hong Kong University of Science and Technology, Hong Kong, China)
Article Search Info Artifacts Available Artifacts Functional
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
Alejandro Aguirre ORCID logo, Philipp G. Haselwarter ORCID logo, Markus de Medeiros ORCID logo, Kwing Hei Li ORCID logo, Simon Oddershede Gregersen ORCID logo, Joseph Tassarotti ORCID logo, and Lars BirkedalORCID logo
(Aarhus University, Denmark; New York University, USA)
Preprint Artifacts Available Artifacts Reusable
Example-Based Reasoning about the Realizability of Polymorphic Programs
Niek Mulleners ORCID logo, Johan Jeuring ORCID logo, and Bastiaan Heeren ORCID logo
(Utrecht University, Netherlands; Open Universiteit, Netherlands)
Article Search Artifacts Available Artifacts Reusable
Snapshottable Stores
Clément Allain ORCID logo, Basile Clément ORCID logo, Alexandre Moine ORCID logo, and Gabriel SchererORCID logo
(Inria, France; OCamlPro, France)
Article Search
Beyond Trees: Calculating Graph-Based Compilers (Functional Pearl)
Patrick BahrORCID logo and Graham Hutton ORCID logo
(IT University of Copenhagen, Denmark; University of Nottingham, United Kingdom)
Article Search Artifacts Available Artifacts Reusable
Grokking the Sequent Calculus (Functional Pearl)
David BinderORCID logo, Marco Tzschentke ORCID logo, Marius Müller ORCID logo, and Klaus Ostermann ORCID logo
(University of Tübingen, Germany)
Preprint Info Artifacts Available Artifacts Reusable
Sound Borrow-Checking for Rust via Symbolic Semantics
Son HoORCID logo, Aymeric Fromherz ORCID logo, and Jonathan ProtzenkoORCID logo
(Inria, France; Microsoft Azure Research, USA)
Preprint Artifacts Available Artifacts Reusable
Abstracting Effect Systems for Algebraic Effect Handlers
Takuma Yoshioka ORCID logo, Taro Sekiyama ORCID logo, and Atsushi IgarashiORCID logo
(Kyoto University, Japan; National Institute of Informatics, Japan)
Article Search Archive submitted (740 kB)
Oxidizing OCaml with Modal Memory Management
Anton Lorenzen ORCID logo, Leo White ORCID logo, Stephen Dolan ORCID logo, Richard A. Eisenberg ORCID logo, and Sam Lindley ORCID logo
(University of Edinburgh, United Kingdom; Jane Street, United Kingdom; Jane Street, USA)
Article Search Archive submitted (890 kB)
Blame-Correct Support for Receiver Properties in Recursively-Structured Actor Contracts
Bram Vandenbogaerde ORCID logo, Quentin Stiévenart ORCID logo, and Coen De Roover ORCID logo
(Vrije Universiteit Brussel, Belgium; Université du Québec à Montréal, Canada)
Article Search Artifacts Available Artifacts Reusable
Gradual Indexed Inductive Types
Mara Malewski ORCID logo, Kenji Maillard ORCID logo, Nicolas TabareauORCID logo, and Éric TanterORCID logo
(University of Chile, Chile; Inria, France)
Article Search
Refinement Composition Logic
Youngju Song ORCID logo and Dongjae Lee ORCID logo
(MPI-SWS, Germany; Seoul National University, South Korea)
Article Search
Abstract Interpreters: A Monadic Approach to Modular Verification
Sébastien Michelland ORCID logo, Yannick ZakowskiORCID logo, and Laure Gonnord ORCID logo
(Université Grenoble-Alpes - Grenoble INP - LCIS, France; Inria - ENS de Lyon - CNRS - UCBL1 - LIP - UMR 5668, France)
Article Search Info Artifacts Available Artifacts Reusable
Dependent Ghosts Have a Reflection for Free
Théo Winterhalter ORCID logo
(Inria, France)
Article Search Artifacts Available Artifacts Reusable
Closure-Free Functional Programming in a Two-Level Type Theory
András Kovács ORCID logo
(University of Gothenburg, Sweden)
Article Search Artifacts Available Artifacts Reusable
Staged Compilation with Module Functors
Tsung-Ju Chiang ORCID logo, Jeremy YallopORCID logo, Leo White ORCID logo, and Ningning Xie ORCID logo
(University of Toronto, Canada; University of Cambridge, United Kingdom; Jane Street, United Kingdom)
Article Search
Deriving with Derivatives: Optimizing Incremental Fixpoints for Higher-Order Flow Analysis
Benjamin Quiring ORCID logo and David Van HornORCID logo
(University of Maryland at College Park, USA; University of Maryland, USA)
Article Search Artifacts Available Artifacts Functional
Parallel Algebraic Effect Handlers
Ningning Xie ORCID logo, Daniel D. Johnson ORCID logo, Dougal Maclaurin ORCID logo, and Adam Paszke ORCID logo
(University of Toronto, Canada; Google DeepMind, Canada; Google DeepMind, USA; Google DeepMind, Germany)
Article Search
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 ORCID logo, Irene Yoon ORCID logo, Hanxi Chen ORCID logo, Yannick ZakowskiORCID logo, and Steve ZdancewicORCID logo
(University of Pennsylvania, USA; Inria, France; Inria - ENS de Lyon - CNRS - UCBL1 - LIP - UMR 5668, France)
Preprint Artifacts Available Artifacts Functional
CCLemma: E-Graph Guided Lemma Discovery for Inductive Equational Proofs
Cole Kurashige ORCID logo, Ruyi Ji ORCID logo, Aditya Giridharan ORCID logo, Mark Barbone ORCID logo, Daniel Noor ORCID logo, Shachar Itzhaky ORCID logo, Ranjit Jhala ORCID logo, and Nadia Polikarpova ORCID logo
(University of California at San Diego, USA; Peking University, China; Technion, Israel)
Article Search Artifacts Available Artifacts Reusable
Call-by-Unboxed-Value
Paul DownenORCID logo
(University of Massachusetts at Lowell, USA)
Article Search
Contextual Typing
Xu Xue ORCID logo and Bruno C. d. S. OliveiraORCID logo
(University of Hong Kong, China)
Article Search Artifacts Available Artifacts Reusable
Specification and Verification for Unrestricted Algebraic Effects and Handling
Yahui Song ORCID logo, Darius Foo ORCID logo, and Wei-Ngan ChinORCID logo
(National University of Singapore, Singapore)
Article Search Artifacts Available Artifacts Functional
Synchronous Programming with Refinement Types
Jiawei Chen ORCID logo, José Luiz Vargas de Mendonça ORCID logo, Bereket Shimels Ayele ORCID logo, Bereket Ngussie Bekele ORCID logo, Shayan Jalili ORCID logo, Pranjal Sharma ORCID logo, Nicholas Wohlfeil ORCID logo, Yicheng Zhang ORCID logo, and Jean-Baptiste Jeannin ORCID logo
(University of Michigan at Ann Arbor, USA; Addis Ababa Institute of Technology, Ethiopia)
Article Search Artifacts Available Artifacts Reusable
Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System
Satoshi Kura ORCID logo and Hiroshi UnnoORCID logo
(National Institute of Informatics, Japan; University of Tsukuba, Japan)
Article Search Artifacts Available Artifacts Reusable
A Coq Mechanization of JavaScript Regular Expression Semantics
Noé De Santo ORCID logo, Aurèle Barrière ORCID logo, and Clément Pit-Claudel ORCID logo
(EPFL, Switzerland)
Article Search Artifacts Available Artifacts Reusable

proc time: 5.83