PPaperPicks
← All conferences
Editions20262025

ICFP 2026

A

International Conference on Function Programming

Official site ↗
39
accepted papers
122
authors
August 24 - 29, 2026
dates
United States
location

39 / 39 papers

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