Chair: Steve Zdancewic.

• Inlining as a space optimization: a simple time- and space-invariant implementation of the weak lambda-calculus — Balabonski (Distinguished, remote) DOI
• First-Class Constrained Types: Elaboration, Type Inference, Approximation, and a Characterization of Termination — Lam, Ferrari-Dominguez, Parreaux (Distinguished) DOI
• Programmable Property-Based Testing — Keles, Frank, Mert, Goldstein, Lampropoulos (Distinguished) DOI
• A Catenable, Splittable, Transient Sequence Data Structure — Charguéraud, Pottier (Distinguished) DOI
• Adapting the MVVM pattern to C++ frontends and Agda-based backends — Csimma (JFP First Paper)

Programmable PBT is the session's essential paper for anyone who writes generators. The claim is that generator construction should itself be a programmable interface rather than a fixed combinator library — which is the same question the Hegel universal-PBT protocol asks from the other end.

Chair: Mae Milano.

• Tail Modulo Async-Await — Nardino, Henrio, Radanne, Zakowski (remote) DOI
• Set-Theoretic Types for Erlang in Practice — Schimpf, Bieniusa (remote) DOI
• Mode Crossing — Peters, Jacobs, Kalinichenko, Stevenson, Smith, Dreyer, Eisenberg DOI
• A Separation Logic for Parallel Time Complexity with Work and Span Credits — Moine, Westrick, Tassarotti DOI
• LoCalMem: Type-Directed Adaptive Serialization for Location- and Content-Addressable Memory — Rainey, Borkowski, Vollmer, Koparkar, Kainen, Singhal DOI

Mode Crossing is the Jane Street/MPI-SWS OxCaml mode system in the open. The Moine/Westrick/Tassarotti separation logic turns cost into a resource you carry in the proof — work and span as credits, spent like permissions.

Chair: Leonidas Lampropoulos.

• Another Type Inference Algorithm for First-class Implicit Polymorphism — Morris DOI
• Same Coeffect, Different Base: Connecting Two Dominant Approaches to Graded Types — Liepelt, Marshall, Orchard DOI
• Towards a Higher-Order Bialgebraic Denotational Semantics — Goncharov, Peressotti, Tsampas, Urbat, Volpe DOI
• LazyHMC: Hamiltonian Monte Carlo simulation for lazy, infinite dimensional probabilistic programs — Craciun, Ong, Schrijvers, Staton DOI
• Imprecise Probabilistic Programming, Precisely (Functional Pearl) — Liell-Cock, Staton DOI

Followed by industrial sponsor introductions at 17:00 and the poster reception 17:30–21:30 in the Auditorium Lobby and Slate Hallway.

Chair: Benjamin Delaware.

• QuickChecking Convergence of Rewriting Systems (Functional Pearl) — Claessen (remote) DOI
• Safety First: How to Safely Disregard Unsafe Behaviour in Compiler Calculations — Bahr (remote) DOI
• Assertions for Free: Transferring Invariants from Algorithm to Implementation Proofs (Functional Pearl) — Wu, Yang, Wu, Cao DOI
• Package Managers à la Carte — Gibb, Ferris, Allsopp, Gazagnaire, Madhavapeddy DOI
• Compositional Generator Equivalence — Vandikas, Sotoudeh, Chechik DOI

Assertions for Free is the refinement-transfer paper: an invariant proved at the algorithm level discharged for free at the implementation level. That is the contract-preservation problem, named.

Chair: Derek Dreyer.

• Bimodels and Biorthogonality for Abstract Machines — Tune, Kavvos DOI
• Let It Be Optimized: Building Multi-Stage Evaluators with Let-Insertion and Optimizations in Small Pieces (Functional Pearl) — Wei, Tan, Zhong DOI
• Animated Pictures for Slide Presentations (Functional Pearl) — Flatt, Findler, Flatt DOI
• Unscanning by Möbius Inversion (Functional Pearl) — Nakano (remote) DOI

Chair: Ben Greenman.

• RunbookFX: Type- and Effect-Safe LLM Synthesis for Executable Incident Diagnosis and Mitigation — Xiao, Li, Ge (remote) DOI
• Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report) — Paraskevopoulou DOI
• Proofs Promptly: Proof-Oriented Programming with AI Agents (Experience Report) — Ioannidis, Swamy, Ebner, Philipose, Ramananandro DOI
• Programming Backpropagation with Reverse Handlers for Arrows — Sanada, Hoshino, Hirai, Katsumata DOI
• On Recursion in Graded Modal Type Theory — Eriksson, Abel, Danielsson DOI

The two experience reports are the closest ICFP has come to admitting the agent question into the papers track. Both take the same position — generate freely, check mechanically — which is the only position that survives contact with a proof assistant. RunbookFX applies the same discipline to incident response: the effect type is the contract on what a synthesized runbook is permitted to touch.

Chair: Sam Westrick.

• Confluence Techniques for Dependent Type Theory with Typed Conversion — Felicissimo, Winterhalter (remote) DOI
• An Equational and Graphical Fixed-Point Calculus (Functional Pearl) — de Mendonça Freire, Gualandi, Nobrega, Paixao (remote) DOI
• Citrus: Algebraic Reasoning About Superconductor Electronics — Kringen, Hardekopf, Sherwood DOI
• Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice — Daggitt, Komendantskaya, Bruni, Teuber, Sirman, Passmore, Smart DOI
• Completeness of Iris-Based Program Logics — Hostert, Zhang, Liu, Gregersen, Jung, Tassarotti DOI

• HMCFA: A Precise and Practical Big-Step Control Flow Analysis for Effect Handlers — Whiting, Germane (remote) DOI
• When Types Intersect and Effects Get Handled — Catozi, Dal Lago, Sekiyama DOI
• Demand-on-Demand Control-Flow Analysis — Kang, Germane DOI
• Adequacy for Predicate Transformer Semantics — Watanabe, Ikebuchi, Kori DOI
• Misquoted No More: Securely Extracting F* Programs with IO — Andrici, Pribisova, Ahman, Hriţcu, Rivas, Winterhalter DOI

Misquoted No More is the extraction-trust paper: what survives the trip from verified F* source to running code with real IO. Extraction is where most verification stories quietly lose their guarantee.

Co-chairs Chris Martens (Northeastern) and William E. Byrd (UAB). The 2026 theme is Relating Relational Languages: cross-pollination with proof assistants, solver-aided tools, Datalog-style languages, and equality saturation.

Pre-prints: Kudasov 2607.25373 · Volkov et al. 2607.24678 · Domoratskiy/Boulytchev 2607.23905. Kudasov's combinators are at https://github.com/fizruk/prune-kanren.

Three of the four talks are performance papers, which is the workshop telling on itself: relational programming's open problem is enumeration order, not expressiveness. Kudasov's defrel/bank memoizes a relation against canonical fresh variables, so a pruned stream is built once and replayed at every call site — the principled version of hand-materializing a transition table, and it keeps the modes that materialization would close off. Volkov et al. attack the same fan-out from the compilation side.

The challenge problem is a text-generation task — bigram models, grammatical category templates, and their composition — with sample solutions in Dusa. That framing sets up the comparison the workshop theme asks for: Datalog- style finite-choice saturation computes a model in one direction, while a unification-based formulation admits generation, checking, infilling, and tagging from a single relation. The mode lattice is where the two formalisms actually differ.

Refutation condition. The claim above fails if finite-choice logic can fill unbound positions by unification rather than enumerate-and-filter. My reading of Dusa says heads must be ground before choice applies, but that has not been pushed on; the PC roster (Rosenblatt, Arntzenius, Willsey) can settle it in one exchange.

Higher-Order Programming with Effects. Six talks, three of them shared with the Paris FPW.

• Teaching Effect Handlers in the Wild — Beneš
• Experience Report: Graph Rewriting with Lexical Effect Handlers — Borner
• Higher-order fork, modally — Boussaa, Tang, Lindley
• Practical Extensions for Graded Monads — Casey, Gaboardi, Katsumata
• Towards Light-Weight Operational Reasoning for Languages with Binders, Categorically — Goncharov
• Modular Storage Mode Analysis — Elsman
• Synthesizing Runners Using Copatterns — Sahoo, Jagannathan
• A Logical Perspective on Capturing Types — Xu (recorded)
• Orbifoldr: Classifying Wallpaper Groups via Functional Image Analysis in Haskell — Jiang, Sharma

Graded monads appear here and again in the ICFP Papers track (Liepelt et al., Eriksson et al.). Grading is having a year.

Functional Art, Music, Modelling and Design. Talks during the day, a public performance at 19:30 with Stephen Taylor's keynote Sonification as (vs.) Program Music and six short pieces.

• Composition: Building Community with Arts, Math, and Code — Mohr, Wang
• AGR: A Rehearsal-to-Performance Workflow for Programming Audio Gestures in Max — Fan
• CounterChoice: Counterpoint Composition in Dusa with a Firmus Foundation — Erdem, Prakash, Angiuli, Bohrer, McCann, Martens, Cong
• Prismriver: Formalization of Music Theory and Algorithmic Composition in Lean 4 — Aniva, Wang
• Demo: The Reduction of Girard's Paradox as Music — Mohr
• Demo: Drawing Algorithms As Modular Objects — Dong, Průša, Wehar, Xu
• The Art of Concert Programming — Gentner

CounterChoice is the crossover: species counterpoint as a finite-choice logic program, same substrate as the miniKanren challenge solutions, same author (Martens) on both. Prismriver is the proof-assistant end of the same question — music theory as a formalized object rather than a generator's implicit prior.

Mentoring workshop. Dreyer on writing papers and giving talks people can follow; Delaware on writing as research practice; Findler on reading reduction semantics; a career panel closing the day.

Remote-streamed from the OCaml Workshop proper. JSON parsing in OxCaml (Pianykh), a new short-paths implementation (Gérard, Anglès d'Auriac, White), a benchmarking service (de Souza Amorim, McGilchrist), first-class docs (Ludlam).

Logic-based synthesis and declarative programming, opened by Theresa Swift and William Byrd. Weirich's keynote on functional/logic programming in Verse is Thursday 14:00, followed by adaptive scheduling (Costantini et al.), negation in ASP (Lierler), and coercive subtyping for algebraic programming (Blanchette, Stump).

Co-hosted rather than a workshop. Opens Friday 09:05 with Ravi Chugh's keynote The Next 700 Block-Based Editors, chaired by Lindsey Kuper.

Regions as Continuation Marks is the one to read closely: region discipline recovered from a control-flow mechanism Racket already has, rather than bolted on as a type-system extension. The R7RS-Large roadmap talk is the standards-process update.

Friday–Saturday. Programs not yet resolved on the schedule page at the time of writing; FUNARCH takes lightning-talk submissions.