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

Title Page

Article: icfp26foreword-fm000-p doi:

Sponsors

Article: icfp26foreword-fm003-p doi:

Editorial Message
Manuel Serrano
(Inria, France; Université Côte d’Azur, France)

Article Search Article: icfp26editorial-fm001-p doi:10.1145/3833372

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

Article Search Article: icfp26main-p12-p doi:10.1145/3828673

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

Article Search Article: icfp26main-p18-p doi:10.1145/3828674

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 Company Limited, China)

Article Search Article: icfp26main-p21-p doi:10.1145/3828675

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 Artifacts Available Artifacts Reusable Article: icfp26main-p23-p doi:10.1145/3828676

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

Article Search Artifacts Available Artifacts Reusable Article: icfp26main-p27-p doi:10.1145/3828677

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

Article Search Article: icfp26main-p29-p doi:10.1145/3828678

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 Artifacts Available Artifacts Reusable Article: icfp26main-p30-p doi:10.1145/3828679

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

Article Search Artifacts Available Artifacts Reusable Article: icfp26main-p34-p doi:10.1145/3828680

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

Article Search Artifacts Available Artifacts Reusable Article: icfp26main-p36-p doi:10.1145/3828681

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 Artifacts Available Artifacts Reusable Article: icfp26main-p39-p doi:10.1145/3828682

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:10.1145/3828683

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

Article Search Artifacts Available Article: icfp26main-p52-p doi:10.1145/3828684

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

Article Search Artifacts Available Artifacts Reusable Article: icfp26main-p56-p doi:10.1145/3828685

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

Article Search Artifacts Available Artifacts Reusable Article: icfp26main-p57-p doi:10.1145/3828686

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

Article Search Article: icfp26main-p59-p doi:10.1145/3828687

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 Artifacts Available Artifacts Functional Article: icfp26main-p60-p doi:10.1145/3828688

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

Article Search Artifacts Available Artifacts Reusable Article: icfp26main-p64-p doi:10.1145/3828689

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

Article Search Artifacts Available Article: icfp26main-p68-p doi:10.1145/3828690

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

Article Search Artifacts Available Artifacts Reusable Article: icfp26main-p71-p doi:10.1145/3828691

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

Article Search Artifacts Available Artifacts Reusable Article: icfp26main-p73-p doi:10.1145/3828692

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:10.1145/3828693

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 Artifacts Available Artifacts Reusable Article: icfp26main-p76-p doi:10.1145/3828694

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

Article Search Artifacts Available Artifacts Reusable Article: icfp26main-p81-p doi:10.1145/3828695

LazyHMC: Hamiltonian Monte Carlo Simulation for Lazy, Infinite Dimensional Probabilistic Programs
Maria-Nicoleta Crăciun, C.-H. 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:10.1145/3828696

Same Coeffect, Different Base: Connecting Two Dominant Approaches to Graded Types
Vilem Liepelt, Danielle Marshall, and Dominic Orchard
(University of Kent, UK; Royal Holloway University of London, UK; University of Cambridge, UK)

Article Search Article: icfp26main-p85-p doi:10.1145/3828697

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

Article Search Article: icfp26main-p87-p doi:10.1145/3828698

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

Article Search Artifacts Available Artifacts Reusable Article: icfp26main-p94-p doi:10.1145/3828699

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

Article Search Artifacts Available Artifacts Reusable Article: icfp26main-p95-p doi:10.1145/3828700

First-Class Constrained Types: Elaboration, Type Inference, Approximation, and a Characterization of Termination
Chun Kit Lam, Florent Ferrari, and Lionel Parreaux
(Hong Kong University of Science and Technology, Hong Kong; ENS de Lyon, France)

Article Search Artifacts Available Artifacts Reusable Article: icfp26main-p97-p doi:10.1145/3828701

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

Article Search Artifacts Available Artifacts Reusable Article: icfp26main-p99-p doi:10.1145/3828702

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:10.1145/3828703

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

Article Search Article: icfp26main-p104-p doi:10.1145/3828704

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

Article Search Article: icfp26main-p107-p doi:10.1145/3828705

A Catenable, Splittable, Transient Sequence Data Structure
Arthur Charguéraud and François Pottier
(Inria, France; Université de Strasbourg, France; CNRS, France)

Article Search Article: icfp26main-p109-p doi:10.1145/3828706

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

Article Search Article: icfp26main-p111-p doi:10.1145/3828707

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

Article Search Article: icfp26main-p114-p doi:10.1145/3828708

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

Article Search Artifacts Available Artifacts Functional Article: icfp26main-p118-p doi:10.1145/3828709

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

Article Search Artifacts Available Artifacts Reusable Article: icfp26main-p120-p doi:10.1145/3828710