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

Title Page

Article: icfp25foreword-fm000-p

Editorial Message

Article: icfp25foreword-fm001-p

Sponsors

Article: icfp25foreword-fm003-p

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)

Preprint Article: icfp25main-p2-p

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)

Article Search Info Article: icfp25main-p9-p

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

Article Search Article: icfp25main-p10-p

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)

Article Search Article: icfp25main-p13-p

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

Article Search Artifacts Available Article: icfp25main-p14-p

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)

Article Search Artifacts Available Article: icfp25main-p15-p

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

Article Search Info Artifacts Available Article: icfp25main-p21-p

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

Article Search Artifacts Available Article: icfp25main-p23-p

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

Article Search Article: icfp25main-p27-p

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)

Preprint Artifacts Available Article: icfp25main-p28-p

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)

Article Search Artifacts Available Article: icfp25main-p29-p

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)

Article Search Artifacts Available Article: icfp25main-p30-p

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)

Article Search Article: icfp25main-p32-p

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

Article Search Article: icfp25main-p33-p

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)

Article Search Artifacts Available Article: icfp25main-p35-p

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

Article Search Artifacts Available Article: icfp25main-p37-p

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)

Article Search Artifacts Available Article: icfp25main-p38-p

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)

Preprint Artifacts Available Article: icfp25main-p41-p

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

Article Search Artifacts Available Article: icfp25main-p50-p

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

Article Search Info Article: icfp25main-p55-p

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)

Article Search Article: icfp25main-p58-p

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

Article Search Info Artifacts Available Article: icfp25main-p61-p

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)

Article Search Article: icfp25main-p64-p

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)

Article Search Article: icfp25main-p69-p

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)

Preprint Article: icfp25main-p70-p

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

Article Search Article: icfp25main-p72-p

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

Article Search Artifacts Available Article: icfp25main-p73-p

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

Article Search Article: icfp25main-p77-p

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

Article Search Artifacts Available Article: icfp25main-p79-p

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

Article Search Article: icfp25main-p81-p

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)

Article Search Info Artifacts Available Article: icfp25main-p82-p

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
(Unaffiliated, USA; National University of Singapore, Singapore)

Article Search Artifacts Available Article: icfp25main-p95-p

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

Article Search Artifacts Available Article: icfp25main-p100-p

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

Article Search Article: icfp25main-p102-p

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

Article Search Article: icfp25main-p104-p

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

Article Search Article: icfp25main-p113-p