ICFP 2026
Proceedings of the ACM on Programming Languages, Volume 10, Number ICFP

Title Page


Article: icfp26foreword-fm000-p doi:

Editorial Message


Article: icfp26foreword-fm001-p doi:

Sponsors


Article: icfp26foreword-fm003-p doi:

An Equational and Graphical Fixed-Point Calculus (Functional Pearl)
Gustavo de Mendonça Freire, Hugo Musso Gualandi, Hugo Nobrega, and Joao Paixao
(Universidade Federal do Rio de Janeiro, Brazil)


Article Search Article: icfp26main-p12-p doi:

Adequacy for Predicate Transformer Semantics
Kazuki Watanabe, Mirai Ikebuchi, and Mayuko Kori
(National Institute of Informatics, Japan; Kyoto University, Japan; Research Institute for Mathematical Sciences, Kyoto University, Japan)


Article Search Article: icfp26main-p18-p doi:

RunbookFX: Type- and Effect-Safe LLM Synthesis for Executable Incident Diagnosis and Mitigation
Yifan Xiao, Shijie Li, and Yuhao Ge
(Peking University, China; China Southern Power Grid, China)


Article Search Article: icfp26main-p21-p doi:

Let It Be Optimized: Building Multi-Stage Evaluators with Let-Insertion and Optimizations in Small Pieces (Functional Pearl)
Guannan Wei, Jun Tan, and Dinghong Zhong
(Tufts University, USA; Independent, China)


Article Search Article: icfp26main-p23-p doi:

On Recursion in Graded Modal Type Theory
Oskar Eriksson, Andreas Abel, and Nils Anders Danielsson
(Department of Computer Science and Engineering, University of Gothenburg and Chalmers University of Technology, Gothenburg, Sweden)


Article Search Article: icfp26main-p27-p doi:

QuickChecking Convergence of Rewriting Systems (Functional Pearl)
Koen Claessen
(Chalmers University of Technology, Sweden)


Article Search Article: icfp26main-p29-p doi:

A Separation Logic for Parallel Time Complexity with Work and Span Credits
Alexandre Moine, Sam Westrick, and Joseph Tassarotti
(New York University, USA)


Article Search Article: icfp26main-p30-p doi:

Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice
Matthew L. Daggitt, Ekaterina Komendantskaya, Alessandro Bruni, Samuel Teuber, Alistair Sirman, Grant Passmore, and Josh Smart
(University of Western Australia, Australia; University of Southampton, UK; IT-University of Copenhagen, Denmark; Karlsruhe Institute of Technology, Germany; Imandra,)


Article Search Article: icfp26main-p34-p doi:

Mode Crossing
Benjamin Peters, Jules Jacobs, Diana Kalinichenko, Liam Stevenson, Aspen Smith, Derek Dreyer, and Richard A. Eisenberg
(MPI-SWS, Germany; Jane Street, USA; Jane Street,)


Article Search Article: icfp26main-p36-p doi:

Completeness of Iris-Based Program Logics
Johannes Hostert, Zichen Zhang, Puming Liu, Simon Oddershede Gregersen, Ralf Jung, and Joseph Tassarotti
(ETH Zurich, Switzerland; New York University, USA; NYU Shanghai, China; CISPA Helmholtz Center for Information Security, Germany)


Article Search Article: icfp26main-p39-p doi:

Safety First: How to Safely Disregard Unsafe Behaviour in Compiler Calculations
Patrick Bahr
(IT University of Copenhagen, Denmark)


Article Search Article: icfp26main-p43-p doi:

Tail Modulo Async-Await
Emma Nardino, Ludovic Henrio, Gabriel Radanne, and Yannick Zakowski
(ENS de Lyon, France; CNRS, France; Inria Lyon, France; Inria Paris, France)


Article Search Article: icfp26main-p52-p doi:

Programmable Property-Based Testing
Alperen Keles, Justine Frank, Ceren Mert, Harrison Goldstein, and Leonidas Lampropoulos
(University of Maryland, College Park, USA; University at Buffalo, SUNY, USA)


Article Search Article: icfp26main-p56-p doi:

Bimodels and Biorthogonality for Abstract Machines
April Tune and G. A. Kavvos
(University of Bristol, UK)


Article Search Article: icfp26main-p57-p doi:

Demand-on-Demand Control-Flow Analysis
Chahyun Kang and Kimball Germane
(Brigham Young University, USA)


Article Search Article: icfp26main-p59-p doi:

LoCalMem: Type-Directed Adaptive Serialization for Location- and Content-Addressable Memory
Michael Rainey, Michael H. Borkowski, Michael Vollmer, Chaitanya S. Koparkar, Mikah Kainen, and Vidush Singhal
(Carnegie Mellon University, USA; Purdue University, USA; University of Kent, UK; MathWorks, USA)


Article Search Article: icfp26main-p60-p doi:

Misquoted No More: Securely Extracting F* Programs with IO
Cezar-Constantin Andrici, Abigail Pribisova, Danel Ahman, Catalin Hritcu, Exequiel Rivas, and Théo Winterhalter
(MPI-SP, Germany; MPI-SP and MPI-SWS, Germany; University of Tartu, Estonia; Tallinn University of Technology, Estonia; Inria Saclay, LMF, France)


Article Search Article: icfp26main-p64-p doi:

Citrus: Algebraic Reasoning about Superconductor Electronics
Harlan Kringen, Ben Hardekopf, and Timothy Sherwood
(University of California at Santa Barbara, USA)


Article Search Article: icfp26main-p68-p doi:

Confluence Techniques for Dependent Type Theory with Typed Conversion
Thiago Felicissimo and Théo Winterhalter
(Inria Rennes, France; Inria Saclay, LMF, France)


Article Search Article: icfp26main-p71-p doi:

Animated Pictures for Slide Presentations (Functional Pearl): From the Shallows to the Depths of a Domain-Specific Language
Oliver Flatt, Robert Bruce Findler, and Matthew Flatt
(University of Washington, USA; Northwestern University, USA; University of Utah, USA)


Article Search Article: icfp26main-p73-p doi:

Towards a Higher-Order Bialgebraic Denotational Semantics
Sergey Goncharov, Marco Peressotti, Stelios Tsampas, Henning Urbat, and Stefano Volpe
(University of Birmingham, UK; University of Southern Denmark, Denmark; University of Erlangen-Nuremberg, Germany)


Article Search Article: icfp26main-p75-p doi:

Assertions for Free: Transferring Invariants from Algorithm to Implementation Proofs (Functional Pearl)
Shushu Wu, Chengxi Yang, Xiwei Wu, and Qinxiang Cao
(Shanghai Jiao Tong University, China)


Article Search Article: icfp26main-p76-p doi:

Compositional Generator Equivalence
Anthony Vandikas, Kiarash Sotoudeh, and Marsha Chechik
(University of Toronto, Canada)


Article Search Article: icfp26main-p81-p doi:

LazyHMC: Hamiltonian Monte Carlo Simulation for Lazy, Infinite Dimensional Probabilistic Programs
Maria-Nicoleta Craciun, Luke Ong, Tom Schrijvers, and Sam Staton
(University of Oxford, UK; Nanyang Technological University, Singapore; KU Leuven, Belgium)


Article Search Article: icfp26main-p82-p doi:

Same Coeffect, Different Base: Connecting Two Dominant Approaches to Graded Types
Vilem-Benjamin Liepelt, Danielle Marshall, and Dominic A. Orchard
(University of Kent, UK; University of Glasgow, UK; University of Cambridge and University of Kent, UK)


Article Search Article: icfp26main-p85-p doi:

Imprecise Probabilistic Programming, Precisely (Functional Pearl): Credal Sets via Graded Monads, BDDs, and Semiring-Parametric Inference
Jack Liell-Cock and Sam Staton
(University of Oxford, UK)


Article Search Article: icfp26main-p87-p doi:

Package Managers à la Carte
Ryan T. Gibb, Patrick Ferris, David Allsopp, Thomas Gazagnaire, and Anil Madhavapeddy
(University of Cambridge, UK; Jane Street,; Tarides, France)


Article Search Article: icfp26main-p94-p doi:

Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report)
Zoe Paraskevopoulou
(National Technical University of Athens, Greece)


Article Search Article: icfp26main-p95-p doi:

An Exploration of First-Class Constrained Types: Semantics, Soundness, Principal Type Inference, and a Characterization of Termination
Lionel Parreaux, Chun Kit Lam, and Florent Ferrari
(HKUST (The Hong Kong University of Science and Technology), Hong Kong; HKUST (The Hong Kong University of Science and Technology), China; ENS de Lyon, France)


Article Search Article: icfp26main-p97-p doi:

Another Type Inference Algorithm for First-Class Implicit Polymorphism
J. Garrett Morris
(University of Iowa, USA)


Article Search Article: icfp26main-p99-p doi:

HMCFA: A Precise and Practical Big-Step Control Flow Analysis for Effect Handlers
Tim Whiting and Kimball Germane
(Brigham Young University, USA)


Article Search Article: icfp26main-p102-p doi:

Programming Backpropagation with Reverse Handlers for Arrows
Takahiro Sanada, Keisuke Hoshino, Kenshin Hirai, and Shin-ya Katsumata
(Fukui Prefectural University, Japan; Research Institute for Mathematical Sciences, Kyoto University, Japan; Kyoto Sangyo University, Japan)


Article Search Article: icfp26main-p104-p doi:

Inlining as a Space Optimization: A Simple Time- and Space-Invariant Implementation of the Weak Lambda-Calculus
Thibaut Balabonski
(LMF, Université Paris-Saclay, France)


Article Search Article: icfp26main-p107-p doi:

A Catenable, Splittable, Transient Sequence Data Structure
Arthur Charguéraud and Francois Pottier
(Inria, France)


Article Search Article: icfp26main-p109-p doi:

When Types Intersect and Effects Get Handled
Stefano Catozi, Ugo Dal Lago, and Taro Sekiyama
(LIPN, France; Bologna, Italy; National Institute of Informatics, Japan)


Article Search Article: icfp26main-p111-p doi:

Set-Theoretic Types for Erlang in Practice
Albert Schimpf and Annette Bieniusa
(University of Kaiserslautern-Landau (RPTU), Germany)


Article Search Article: icfp26main-p114-p doi:

Proofs Promptly: An Experience Report on Proof-Oriented Programming with AI Agents
Eleftherios Ioannidis, Nikhil Swamy, Gabriel Ebner, Matthai Philipose, and Tahina Ramananandro
(Microsoft Research, USA)


Article Search Article: icfp26main-p118-p doi:

Unscanning by Möbius Inversion (Functional Pearl)
Keisuke Nakano
(Tohoku University, Japan)


Article Search Article: icfp26main-p120-p doi: