ICFP 2025
Proceedings of the ACM on Programming Languages, Volume 9, Number ICFP

Title Page

Editorial Message

Sponsors

A Bargain for Mergesorts: How to Prove Your Mergesort Correct and Stable, Almost for Free
Cyril Cohen and Kazuhiko Sakaguchi
(Inria - CNRS - ENS Lyon - Université Claude Bernard Lyon 1 - LIP - UMR 5668, France; CNRS - ENS Lyon - Université Claude Bernard Lyon 1 - LIP - UMR 5668, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Frex: Dependently Typed Algebraic Simplification
Guillaume Allais, Edwin Brady, Nathan Corbyn, Ohad Kammar, and Jeremy Yallop
(University of Strathclyde, UK; University of St. Andrews, UK; University of Oxford, UK; University of Edinburgh, UK; University of Cambridge, UK)

Publisher's Version Info

Robust Dynamic Embedding for Gradual Typing
Koen Jacobs, Matías Toro, Nicolas Tabareau, and Éric Tanter
(Inria, France; University of Chile, Chile)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Normalization by Evaluation for Non-cumulativity
Shengyi Jiang, Jason Z. S. Hu, and Bruno C. d. S. Oliveira
(University of Hong Kong, China; Amazon, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Formal Semantics and Program Logics for a Fragment of OCaml
Remy Seassau, Irene Yoon, Jean-Marie Madiot, and François Pottier
(Inria, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
Marcos Grandury, Aleksandar Nanevski, and Alexander Gryzlov
(IMDEA Software Institute, Spain; Universidad Politécnica de Madrid, Spain)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

McTT: A Verified Kernel for a Proof Assistant
Junyoung Jang, Antoine Gaulin, Jason Z. S. Hu, and Brigitte Pientka
(McGill University, Canada; Amazon, USA)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable

Almost Fair Simulations
Arthur Correnson, Iona Kuhn, and Bernd Finkbeiner
(CISPA Helmholtz Center for Information Security, Germany; Saarland University, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Bialgebraic Reasoning on Stateful Languages
Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat
(University of Birmingham, UK; Friedrich-Alexander University Erlangen-Nürnberg, Germany; University of Southern Denmark, Denmark)

Publisher's Version

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Philipp G. Haselwarter, Joseph Tassarotti, and Lars Birkedal
(Aarhus University, Denmark; New York University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Reasoning about Weak Isolation Levels in Separation Logic
Anders Alnor Mathiasen, Léon Gondelman, Léon Ducruet, Amin Timany, and Lars Birkedal
(Aarhus University, Denmark; Aalborg University, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages
J. A. Carr, Benjamin Quiring, John Reppy, Olin Shivers, Skye Soss, and Byron Zhong
(University of Chicago, USA; University of Maryland at College Park, USA; Northeastern University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Polynomial-Time Program Equivalence for Machine Knitting
Nathan Hurtig, Jenny Han Lin, Thomas S. Price, Adriana Schulz, James McCann, and Gilbert Louis Bernstein
(University of Washington, USA; University of Utah, USA; Carnegie Mellon University, USA)

Publisher's Version

Multi-stage Programming with Splice Variables
Tsung-Ju Chiang and Ningning Xie
(University of Toronto, Canada)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Fusing Session-Typed Concurrent Programming into Functional Programming
Chuta Sano, Deepak Garg, Ryan Kavanagh, Brigitte Pientka, and Bernardo Toninho
(McGill University, Canada; MPI-SWS, Germany; Université du Québec à Montréal, Canada; Instituto Superior Técnico - University of Lisbon, Portugal)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Truly Functional Solutions to the Longest Uptrend Problem (Functional Pearl)
Alexander Dinges and Ralf Hinze
(RPTU Kaiserslautern-Landau, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Quantum Hardware
Liyi Li, David Young, James Bryan Graves, Chandeepa Dissanayake, and Amr Sabry
(Iowa State University, USA; University of Kansas, USA; Indiana University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

SecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F*
Cezar-Constantin Andrici, Danel Ahman, Cătălin Hriţcu, Ruxandra Icleanu, Guido Martínez, Exequiel Rivas, and Théo Winterhalter
(MPI-SP, Germany; University of Tartu, Estonia; University of Edinburgh, UK; Microsoft Research, USA; Tallinn University of Technology, Estonia; Inria, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Effectful Lenses: There and Back with Different Monads
Ruifeng Xie, Tom Schrijvers, and Zhenjiang Hu
(Peking University, China; KU Leuven, Belgium)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Correctness Meets Performance: From Agda to Futhark
Artjoms Šinkarovs and Troels Henriksen
(University of Southampton, UK; University of Copenhagen, Denmark)

Publisher's Version Info

Functional Networking for Millions of Docker Desktops (Experience Report)
Anil Madhavapeddy, David J. Scott, Patrick Ferris, Ryan T. Gibb, and Thomas Gazagnaire
(University of Cambridge, UK; Docker, UK; Tarides, France)

Publisher's Version

Fulls Seldom Differ
Mark Koch, Alan Lawrence, Conor McBride, and Craig Roy
(Quantinuum, UK; University of Strathclyde, UK)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Functional

2-Functoriality of Initial Semantics, and Applications
Benedikt Ahrens, Ambroise Lafont, and Thomas Lamiaux
(Delft University of Technology, Netherlands; LIX - Ecole Polytechnique, France; Inria, France; Nantes University, France)

Publisher's Version

CRDT Emulation, Simulation, and Representation Independence
Nathan Liittschwager, Jonathan Castello, Stelios Tsampas, and Lindsey Kuper
(University of California at Santa Cruz, USA; University of Southern Denmark, Denmark)

Publisher's Version

Multiple Resumptions and Local Mutable State, Directly
Serkan Muhcu, Philipp Schuster, Michel Steuwer, and Jonathan Immanuel Brachthäuser
(TU Berlin, Germany; University of Tübingen, Germany)

Publisher's Version

First-Order Laziness
Anton Lorenzen, Daan Leijen, Wouter Swierstra, and Sam Lindley
(University of Edinburgh, UK; Microsoft Research, USA; Utrecht University, Netherlands)

Publisher's Version

Linear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl)
Maximilian Doré
(University of Oxford, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Type Universes as Kripke Worlds
Paulette Koronkevich and William J. Bowman
(University of British Columbia, Canada)

Publisher's Version

Teaching Software Specification (Experience Report)
Cameron Moy and Daniel Patterson
(Northeastern University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Compiling with Generating Functions
Jianlin Li and Yizhou Zhang
(University of Waterloo, Canada)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Type Theory in Type Theory using a Strictified Syntax
Ambrus Kaposi and Loïc Pujet
(Eötvös Loránd University, Hungary; Stockholm University, Sweden)

Publisher's Version Published Artifact Info Artifacts Available

Pushing the Information-Theoretic Limits of Random Access Lists: Traversing Cons Lists in(1 + 1/𝜎) ⌊lg 𝑛⌋ + 𝜎 + 9 Steps
Edward Peters, Yong Qi Foo, and Michael D. Adams
(Independent, USA; National University of Singapore, Singapore)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Verified Interpreters for Dynamic Languages with Applications to the Nix Expression Language
Rutger Broekhoff and Robbert Krebbers
(Radboud University Nijmegen, Netherlands)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Relax! The Semilenient Core of Choreographic Programming (Functional Pearl)
Dan Plyukhin, Xueying Qin, and Fabrizio Montesi
(University of Southern Denmark, Denmark)

Publisher's Version

Call-Guarded Abstract Definitional Interpreters
Kimball Germane
(Brigham Young University, USA)

Publisher's Version

Big Steps in Higher-Order Mathematical Operational Semantics
Sergey Goncharov, Pouya Partow, and Stelios Tsampas
(University of Birmingham, UK; University of Southern Denmark, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable