ICFP 2025
who it's for
programming language researchers, functional programmers, proof engineers, language designers, compiler engineers, programming language educators, systems implementers
topics
robust dynamic embedding for gradual typing; call-guarded definitional interpreters; multiple-resumption effect handlers; substitution strictified type theory; CRDT emulation and simulation; separation logic for weak isolation; lazy constructors for laziness; information-theoretic random access lists; choreographic programming semilenient core; verified interpreters for dynamic languages; linear types with dynamic multiplicities; compiling with generating functions
| title | author | length |
|---|---|---|
| Robust Dynamic Embedding for Gradual Typing | Koen Jacobs, Matías Toro, Nicolas Tabareau, Éric Tanter | 25m |
Defines Robust Dynamic Embedding as a new adequacy criterion: if a dynamic component semantically satisfies a static type then its embedding ascribed to that… | ||
| SIGPLAN AV Report | Eloise Christian, Guilherme Espada | 07m |
Volunteer-run SIGPLAN AV manages room audio, streaming, recording and archival for about 50 live streams, covering roughly 600 talks (about 45 pre-recorded or… | ||
| Call-Guarded Abstract Definitional Interpreters | Kimball Germane | 25m |
A hybrid definitional interpreter called CGADI runs concrete semantics until a parameterized call guard forces abstraction, proving computability when the… | ||
| Multiple Resumptions and Local Mutable State, Directly | Serkan Muhcu, Philipp Schuster, Michel Steuwer, Jonathan Immanuel Brachthäuser | 25m |
A compilation strategy and runtime implement lexical effect handlers that support multiple resumptions plus stack-allocated mutable state by using a linked… | ||
| Type Theory in Type Theory using a Strictified Syntax | Ambrus Kaposi, Loïc Pujet | 26m |
They build an isomorphic, substitution strictified initial CwF that encodes substitutions as meta-level functions so all substitution equations become… | ||
| CRDT Emulation, Simulation, and Representation Independence | Nathan Liittschwager, Jonathan Castello, Stelios Tsampas, Lindsey Kuper | 24m |
Formalizes CRDT emulation as weak simulation between transition systems and gives constructive translations both ways, focusing on the op-based→state-based… | ||
| Teaching Software Specification (Experience Report) | Cameron Moy, Daniel Patterson | 27m |
Course redesign puts software specification front and center for first-year students and builds a tiny custom language that adds contracts and property-based… | ||
| Type Universes as Kripke Worlds | Paulette Koronkevich, William J. Bowman | 26m |
Paper claims that stratifying allocated types into a type universe hierarchy (each universe ↔ a semantic Kripke world per universe) removes the usual… | ||
| Reasoning about Weak Isolation Levels in Separation Logic | Anders Alnor Mathiasen, Léon Gondelman, Léon Ducruet, Amin Timany, Lars Birkedal | 27m |
Paper formalizes three weak isolation levels for key-value transactions and mechanizes them in Rocq on Iris, giving atomic-style separation-logic specs for… | ||
| First-Order Laziness | Anton Lorenzen, Daan Leijen, Wouter Swierstra, Sam Lindley | 27m |
Proposes replacing thunk closures with lazy constructors that are defunctionalized first‑order values, implemented in Koka; evaluation happens on pattern match… | ||
| Pushing the Information-Theoretic Limits of Random Access Lists | Edward Peters, Yong Qi Foo, Michael D. Adams | 23m |
Provides a concrete improvement to Myers lists: a simple variant reduces pointer traversals from 3⌈lg n⌉−5 to 2⌈lg(n+1)⌉−3 and a more complex design uses skip… | ||
| Relax! The Semilenient Core of Choreographic Programming (Functional Pearl) | Dan Plyukhin, Xueying Qin, Fabrizio Montesi | 25m |
Presents a trimmed formal core called λχ with just ten operational rules and a new semilenient evaluation strategy that mixes lenient (evaluate under binders)… | ||
| Big Steps in Higher-Order Mathematical Operational Semantics | Sergey Goncharov, Pouya Partow, Stelios Tsampas | 27m |
Proves an abstract categorical equivalence between small‑step and big‑step for higher‑order SOS by defining a categorical big‑step SOS format and a… | ||
| Almost Fair Simulations | Arthur Correnson, Iona Kuhn, Bernd Finkbeiner | 21m |
Proves that language inclusion for nondeterministic Büchi automata can be established by a family of fairness‑preserving simulations: direct simulation, delay… | ||
| Correctness Meets Performance: From Agda to Futhark | Artjoms Šinkarovs, Troels Henriksen | 24m |
Derives a reverse-mode automatic-differentiation pipeline in Agda for index-safe tensors, proves semantic preservation for AD and optimizer passes, and… | ||
| 2-Functoriality of Initial Semantics, and Applications | Benedikt Ahrens, Ambroise Lafont, Thomas Lamiaux | 26m |
Shows that initial semantics, when parametrized by the monoidal category of contexts, is 2-functorial: a monoidal functor or adjunction between base categories… | ||
| A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Quantum Hardware | Liyi Li, David Young, James Bryan Graves, Chandeepa Dissanayake, Amr Sabry | 27m |
A Haskell library called EnQ expresses optimization problems as energy constraint computations and uses the Traversable and Monad abstractions to build final… | ||
| JFP Announcement | Derek Dreyer | 05m |
Cambridge University Press is dropping the Journal of Functional Programming at end of 2025 and ownership is transferring to the editors with a planned move to… | ||
| Effectful Lenses: There and Back with Different Monads | Ruifeng Xie, Tom Schrijvers, Zhenjiang Hu | 21m |
Framework introduces effectful lenses that allow different monads in the two directions, using the lenses with complements encoding plus user-specified… | ||
| Truly Functional Solutions to the Longest Uptrend Problem (Functional Pearl) | Alexander Dinges, Ralf Hinze | 24m |
Replaces the array-based LIS implementation with purely functional structures, shows a first persistent-sequence version runs about 6× slower, then builds a… | ||
| Functional Networking for Millions of Docker Desktops (Experience Report) | Anil Madhavapeddy, David J. Scott, Patrick Ferris, Ryan T. Gibb, Thomas Gazagnaire | 25m |
A decade-long engineering saga that ships OCaml unikernels inside Docker Desktop, running Linux as a callable library via a library virtual machine monitor and… | ||
| Fulls Seldom Differ | Mark Koch, Alan Lawrence, Conor McBride, Craig Roy | 25m |
Introduces a restricted language of natural number expressions that covers doubling, iterated doubling (exponentiation), and a full operator for 2^n−1 and… | ||
| PC Chair Report | Dominique Devriese | 13m |
Program committee reports 110 submissions and 36 acceptances (≈33%), with nine JFP journal‑first papers included. A two‑round process enforces mandatory… | ||
| Opening | Ilya Sergey | 05m |
Venue is Marina Bay Sands convention center with Orchid Plenary as the main room and lunches in Orchid Dining Hall; streaming runs from the Orchid West area… | ||
| Award Ceremony | Dominique Devriese, Ilya Sergey | 16m |
Selection process reports that 10 papers nominated are reviewed by a committee of six senior non‑conflicted members who meet twice and pick four distinguished… | ||
| Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs | Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal | 24m |
Presents Coneris, the first higher-order concurrent separation logic that proves numeric error bounds for concurrent probabilistic programs and mechanizes all… | ||
| Normalization by Evaluation for Non-cumulativity | Shengyi Jiang, Jason Z. S. Hu | 21m |
Claims that untyped NbE for non-cumulativity is sound and complete for a Martin-Löf style type theory with explicit universe levels, gives a mechanized proof… | ||
| Polynomial-Time Program Equivalence for Machine Knitting | Nathan Hurtig, Jenny Han Lin, Thomas S. Price, Adriana Schulz, James McCann, Gilbert Louis Bernstein | 24m |
An algorithm canonicalizes algebraic representations of knitting-program string diagrams into a normal form, reducing program equivalence to comparing those… | ||
| General Chair Report | Ilya Sergey | 13m |
About 600 on-site registrations, roughly half students, and about 30 collocated events; organizers report nearly 70 student volunteers, nine dedicated AV… | ||
| Verified Interpreters for Dynamic Languages with Applications to the Nix Expression(…) | Rutger Broekhoff, Robbert Krebbers | 21m |
Paper presents a substitution-based operational semantics using deferred substitutions for dynamic name binding, extends call-by-name lambda calculus to model… | ||
| Bialgebraic Reasoning on Stateful Languages | Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, Henning Urbat | 22m |
Proposes a concrete operational encoding that splits programs into readers (expecting an input store) and writers (running computations tagged with a store)… | ||
| A Bargain for Mergesorts: How to Prove Your Mergesort Correct and Stable, Almost for Free | Cyril Cohen, Kazuhiko Sakaguchi | 26m |
Proves that a mergesort implementation satisfying a specific characteristic property yields correctness (sorted + permutation) and stability, for many… | ||
| 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, Théo Winterhalter | 25m |
SecRef is a secure-compilation framework for F that enforces verified programs’ assumptions about dynamically shared ML-style mutable references by inserting… | ||
| ICFP 2026 Announcement | Sam Tobin-Hochstadt | 05m |
ICFP 2026 takes place in Indianapolis on the brand new IU Indianapolis campus with the main conference in Hine Hall and workshops in University Tower; primary… | ||
| Formal Semantics and Program Logics for a Fragment of OCaml | Remy Seassau, Irene Yoon, Jean-Marie Madiot, François Pottier | 24m |
Defines OLang, a sequential OCaml fragment with first-class functions, extensible ADTs, pattern matching, references, exceptions and effect handlers, and gives… | ||
| McTT: A Verified Kernel for a Proof Assistant | Junyoung Jang, Antoine Gaulin, Jason Z. S. Hu, Brigitte Pientka | 25m |
A fully verified kernel for core Martin‑Löf type theory is implemented in Rocq, proving normalization, consistency and injectivity of constructors and proving… | ||
| ICFP Contest Report | Liam O'Connor | 15m |
ICFP programming contest tasks teams to reconstruct randomized maps of a labyrinth whose rooms have six doors and only two‑bit labels; a server returns… | ||
| Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages | J. A. Carr, Benjamin Quiring, John Reppy, Olin Shivers, Skye Soss, Byron Zhong | 24m |
An abstract-interpretation analysis discovers which free-variable bindings are always shared so callers can supply environments instead of heap-allocating… | ||
| Linear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl) | Maximilian Doré | 25m |
Constructs a linear typing discipline inside dependent type theory and implements it in Cubical Agda, using supplies (finite multisets) plus a small set of… | ||
| Fusing Session-Typed Concurrent Programming into Functional Programming | Chuta Sano, Deepak Garg, Ryan Kavanagh, Brigitte Pientka, Bernardo Toninho | 26m |
FuSes embeds a session-typed process calculus inside a pure functional language and ships a formal type system with operational semantics and a machine-checked… | ||
| Compiling with Generating Functions | Jianlin Li, Yizhou Zhang | 24m |
A compiler called Genie compiles probabilistic programs to generating functions as a deterministic target (PIL → DIL) and proves correctness against a… | ||
| Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach | Marcos Grandury, Aleksandar Nanevski, Alexander Gryzlov | 23m |
Graphs become a partial commutative monoid so they support join-based decomposition; structure-preserving PCM morphisms distribute over joins and let proofs… | ||
| nothing matches | ||