ICFP 2025

36 papers

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