PPaperPicks
← All conferences
Editions20262025

ICFP 2025

A

International Conference on Function Programming

Official site ↗
36
accepted papers
121
authors
October 12-18, 2025
dates
Singapore
location

36 / 36 papers

  1. 1
    2-Functoriality of Initial Semantics, and Applications
    Benedikt Ahrens
    ,
    Ambroise Lafont
    ,
    Thomas Lamiaux
  2. 2
    A Bargain for Mergesorts: How to Prove Your Mergesort Correct and Stable, Almost for Free
    Cyril Cohen
    ,
    Kazuhiko Sakaguchi
  3. 3
    A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Quantum Hardware
    Liyi Li
    ,
    David Young
    ,
    James Bryan Graves
    ,
    Chandeepa Dissanayake
    ,
    Amr Sabry
  4. 4
    Almost Fair Simulations
    Arthur Correnson
    ,
    Iona Kuhn
    ,
    Bernd Finkbeiner
  5. 5
    Bialgebraic Reasoning on Stateful Languages
    Sergey Goncharov
    ,
    Stefan Milius
    ,
    Lutz Schröder
    ,
    Stelios Tsampas
    ,
    Henning Urbat
  6. 6
    Big Steps in Higher-Order Mathematical Operational Semantics
    Sergey Goncharov
    ,
    Pouya Partow
    ,
    Stelios Tsampas
  7. 7
    Call-Guarded Abstract Definitional Interpreters
    Kimball Germane
  8. 8
    Compiling with Generating Functions
    Jianlin Li
    ,
    Yizhou Zhang
  9. 9
    Correctness Meets Performance: From Agda to Futhark
    Artjoms Sinkarovs
    ,
    Troels Henriksen
  10. 10
    CRDT Emulation, Simulation, and Representation Independence
    Nathan Liittschwager
    ,
    Jonathan Castello
    ,
    Stelios Tsampas
    ,
    Lindsey Kuper
  11. 11
    Effectful Lenses: There and Back with Different Monads
    Ruifeng Xie
    ,
    Tom Schrijvers
    ,
    Zhenjiang Hu
  12. 12
    Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages
    J. A. Carr
    ,
    Benjamin Quiring
    ,
    John H. Reppy
    ,
    Olin Shivers
    ,
    Skye Soss
    ,
    Byron Zhong
  13. 13
    First-Order Laziness
    Anton Lorenzen
    ,
    Daan Leijen
    ,
    Wouter Swierstra
    ,
    Sam Lindley
  14. 14
    Formal Semantics and Program Logics for a Fragment of OCaml
    Remy Seassau
    ,
    Irene Yoon
    ,
    Jean-Marie Madiot
    ,
    François Pottier
  15. 15
    Frex: Dependently Typed Algebraic Simplification
    Guillaume Allais
    ,
    Edwin C. Brady
    ,
    Nathan Corbyn
    ,
    Ohad Kammar
    ,
    Jeremy Yallop
  16. 16
    Fulls Seldom Differ
    Mark Koch
    ,
    Alan Lawrence
    ,
    Conor McBride
    ,
    Craig Roy
  17. 17
    Functional Networking for Millions of Docker Desktops (Experience Report)
    Anil Madhavapeddy
    ,
    David J. Scott
    ,
    Patrick Ferris
    ,
    Ryan Gibb
    ,
    Thomas Gazagnaire
  18. 18
    Fusing Session-Typed Concurrent Programming into Functional Programming
    Chuta Sano
    ,
    Deepak Garg
    ,
    Ryan Kavanagh
    ,
    Brigitte Pientka
    ,
    Bernardo Toninho
  19. 19
    Linear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl)
    Maximilian Doré
  20. 20
    McTT: A Verified Kernel for a Proof Assistant
    Junyoung Jang
    ,
    Antoine Gaulin
    ,
    Jason Z. S. Hu
    ,
    Brigitte Pientka
  21. 21
    Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
    Kwing Hei Li
    ,
    Alejandro Aguirre
    ,
    Simon Oddershede Gregersen
    ,
    Philipp G. Haselwarter
    ,
    Joseph Tassarotti
    ,
    Lars Birkedal
  22. 22
    Multi-stage Programming with Splice Variables
    Tsung-Ju Chiang
    ,
    Ningning Xie
  23. 23
    Multiple Resumptions and Local Mutable State, Directly
    Serkan Muhcu
    ,
    Philipp Schuster
    ,
    Michel Steuwer
    ,
    Jonathan Immanuel Brachthäuser
  24. 24
    Normalization by Evaluation for Non-cumulativity
    Shengyi Jiang
    ,
    Jason Z. S. Hu
    ,
    Bruno C. d. S. Oliveira
  25. 25
    Polynomial-Time Program Equivalence for Machine Knitting
    Nathan Hurtig
    ,
    Jenny Han Lin
    ,
    Thomas S. Price
    ,
    Adriana Schulz
    ,
    James McCann
    ,
    Gilbert Louis Bernstein
  26. 26
    Pushing the Information-Theoretic Limits of Random Access Lists: Traversing Cons Lists in (1 + 1/𝜎 ) ⌊lg 𝑛⌋ + 𝜎 + 9 Steps
    Edward Peters
    ,
    Yong Qi Foo
    ,
    Michael D. Adams
  27. 27
    Reasoning about Weak Isolation Levels in Separation Logic
    Anders Alnor Mathiasen
    ,
    Léon Gondelman
    ,
    Léon Ducruet
    ,
    Amin Timany
    ,
    Lars Birkedal
  28. 28
    Relax! The Semilenient Core of Choreographic Programming (Functional Pearl)
    Dan Plyukhin
    ,
    Xueying Qin
    ,
    Fabrizio Montesi
  29. 29
    Robust Dynamic Embedding for Gradual Typing
    Koen Jacobs
    ,
    Matías Toro
    ,
    Nicolas Tabareau
    ,
    Éric Tanter
  30. 30
    SecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F
    Cezar-Constantin Andrici
    ,
    Danel Ahman
    ,
    Catalin Hritcu
    ,
    Ruxandra Icleanu
    ,
    Guido Martínez
    ,
    Exequiel Rivas
    ,
    Théo Winterhalter
  31. 31
    Teaching Software Specification (Experience Report)
    Cameron Moy
    ,
    Daniel Patterson
  32. 32
    Truly Functional Solutions to the Longest Uptrend Problem (Functional Pearl)
    Alexander Dinges
    ,
    Ralf Hinze
  33. 33
    Type Theory in Type Theory using a Strictified Syntax
    Ambrus Kaposi
    ,
    Loïc Pujet
  34. 34
    Type Universes as Kripke Worlds
    Paulette Koronkevich
    ,
    William J. Bowman
  35. 35
    Verified Interpreters for Dynamic Languages with Applications to the Nix Expression Language
    Rutger Broekhoff
    ,
    Robbert Krebbers
  36. 36
    Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
    Marcos Grandury
    ,
    Aleksandar Nanevski
    ,
    Alexander Gryzlov