ICFP 2026

39 papers

1. A Catenable, Splittable, Transient Sequence Data Structure · Arthur Charguéraud, François Pottier
2. A Separation Logic for Parallel Time Complexity with Work and Span Credits · Alexandre Moine, Sam Westrick, Joseph Tassarotti
3. Adequacy for Predicate Transformer Semantics · Kazuki Watanabe, Mirai Ikebuchi, Mayuko Kori
4. An Equational and Graphical Fixed-Point Calculus (Functional Pearl) · Gustavo de Mendonça Freire, Hugo Musso Gualandi, Hugo Nobrega, Joao Paixao
5. Animated Pictures for Slide Presentations: From the Shallows to the Depths of a Domain-Specific Language (Functional Pearl) · Oliver Flatt, Robert Bruce Findler, Matthew Flatt
6. Another Type Inference Algorithm for First-Class Implicit Polymorphism · J. Garrett Morris
7. Assertions for Free: Transferring Invariants from Algorithm to Implementation Proofs (Functional Pearl) · Shushu Wu, Chengxi Yang, Xiwei Wu, Qinxiang Cao
8. Bimodels and Biorthogonality for Abstract Machines · April Tune, G. A. Kavvos
9. Citrus: Algebraic Reasoning about Superconductor Electronics · Harlan Kringen, Timothy Sherwood, Ben Hardekopf
10. Completeness of Iris-Based Program Logics · Johannes Hostert, Zichen Zhang, Puming Liu, Simon Oddershede Gregersen, Ralf Jung, Joseph Tassarotti
11. Compositional Generator Equivalence · Anthony Vandikas, Kiarash Sotoudeh, Marsha Chechik
12. 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 + 1 more
13. Confluence Techniques for Dependent Type Theory with Typed Conversion · Thiago Felicissimo, Théo Winterhalter
14. Demand-on-Demand Control-Flow Analysis · Chahyun Kang, Kimball Germane
15. Editorial Message · Manuel Serrano
16. First-Class Constrained Types: Elaboration, Type Inference, Approximation, and a Characterization of Termination · Chun Kit Lam, Florent Ferrari, Lionel Parreaux
17. HMCFA: A Precise and Practical Big-Step Control Flow Analysis for Effect Handlers · Tim Whiting, Kimball Germane
18. Imprecise Probabilistic Programming, Precisely: Credal Sets via Graded Monads, BDDs, and Semiring-Parametric Inference (Functional Pearl) · Jack Liell-Cock, Sam Staton
19. Inlining as a Space Optimization: A Simple Time- and Space-Invariant Implementation of the Weak Lambda-Calculus · Thibaut Balabonski
20. LazyHMC: Hamiltonian Monte Carlo Simulation for Lazy, Infinite Dimensional Probabilistic Programs · Maria-Nicoleta Craciun, C.-H. Luke Ong, Tom Schrijvers, Sam Staton
21. Let It Be Optimized: Building Multi-stage Evaluators with Let-Insertion and Optimizations in Small Pieces (Functional Pearl) · Guannan Wei, Jun Tan, Dinghong Zhong
22. LoCalMem: Type-Directed Adaptive Serialization for Location- and Content-Addressable Memory · Michael Rainey, Michael H. Borkowski, Michael Vollmer, Chaitanya S. Koparkar, Mikah Kainen, Vidush Singhal
23. Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report) · Zoe Paraskevopoulou
24. Misquoted No More: Securely Extracting F* Programs with IO · Cezar-Constantin Andrici, Abigail Pribisova, Danel Ahman, Catalin Hritcu, Exequiel Rivas, Théo Winterhalter
25. Mode Crossing · Benjamin Peters, Jules Jacobs, Diana Kalinichenko, Liam Stevenson, Aspen Smith, Derek Dreyer + 1 more
26. On Recursion in Graded Modal Type Theory · Oskar Eriksson, Andreas Abel, Nils Anders Danielsson
27. Package Managers à la Carte: A Formal Model of Dependency Resolution · Ryan Thomas Gibb, Patrick Ferris, David Allsopp, Thomas Gazagnaire, Anil Madhavapeddy
28. Programmable Property-Based Testing · Alperen Keles, Justine Frank, Ceren Mert, Harrison Goldstein, Leonidas Lampropoulos
29. Programming Backpropagation with Reverse Handlers for Arrows · Takahiro Sanada, Keisuke Hoshino, Kenshin Hirai, Shin-ya Katsumata
30. Proofs Promptly: Proof-Oriented Programming with AI Agents (Experience Report) · Eleftherios Ioannidis, Nikhil Swamy, Gabriel Ebner, Matthai Philipose, Tahina Ramananandro
31. QuickChecking Convergence of Rewriting Systems (Functional Pearl) · Koen Claessen
32. RunbookFX: Type- and Effect-Safe LLM Synthesis for Executable Incident Diagnosis and Mitigation · Yifan Xiao, Shijie Li, Yuhao Ge
33. Safety First: How to Safely Disregard Unsafe Behaviour in Compiler Calculations · Patrick Bahr
34. Same Coeffect, Different Base: Connecting Two Dominant Approaches to Graded Types · Vilem-Benjamin Liepelt, Danielle Marshall, Dominic Orchard
35. Set-Theoretic Types for Erlang in Practice (Experience Report) · Albert Schimpf, Annette Bieniusa
36. Tail Modulo Async-Await · Emma Nardino, Ludovic Henrio, Gabriel Radanne, Yannick Zakowski
37. Towards a Higher-Order Bialgebraic Denotational Semantics · Sergey Goncharov, Marco Peressotti, Stelios Tsampas, Henning Urbat, Stefano Volpe
38. Unscanning by Möbius Inversion (Functional Pearl) · Keisuke Nakano
39. When Types Intersect and Effects Get Handled · Stefano Catozi, Ugo Dal Lago, Taro Sekiyama