Presentations for papers in the Journal of Functional Programming.
Accepted Papers
| Title | |
|---|---|
| A contextual formalization of structural coinduction JFP First Papers DOI | |
| A practical formalization of monadic equational reasoning in dependent-type theory JFP First Papers DOI | |
| A simple blame calculus for explicit nulls JFP First Papers DOI | |
| Binary search—think positive JFP First Papers DOI | |
| Bottom-up computation using trees of sublists JFP First Papers DOI | |
| Domain-specific tensor languages JFP First Papers DOI | |
| How much is in a square? Calculating functional programs with squares JFP First Papers DOI | |
| OCaml Blockly JFP First Papers DOI | |
| You could have invented Fenwick trees JFP First Papers DOI |
Dates
Tracks
This program is tentative and subject to change.
Mon 13 OctDisplayed time zone: Perth change
Mon 13 Oct
Displayed time zone: Perth change
10:50 - 12:05 | |||
10:50 25mTalk | 2-Functoriality of Initial Semantics, and Applications ICFP Papers Benedikt Ahrens Delft University of Technology, Ambroise Lafont Inria, France, Thomas Lamiaux University of Paris-Saclay, Ens Paris-Saclay DOI | ||
11:15 25mTalk | Bialgebraic Reasoning on Stateful Languages ICFP Papers Sergey Goncharov University of Birmingham, Stefan Milius Friedrich-Alexander University Erlangen-Nürnberg, Lutz Schröder Friedrich-Alexander University Erlangen-Nürnberg, Stelios Tsampas University of Southern Denmark, Henning Urbat Friedrich-Alexander University Erlangen-Nürnberg DOI | ||
11:40 25mTalk | Frex: Dependently Typed Algebraic Simplification ICFP Papers Guillaume Allais University of Strathclyde, Edwin Brady University of St. Andrews, Nathan Corbyn University of Oxford, Ohad Kammar University of Edinburgh, Jeremy Yallop University of Cambridge DOI Pre-print | ||
10:50 - 12:05 | |||
10:50 25mTalk | Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages ICFP Papers J. Carr University of Chicago, Benjamin Quiring University of Maryland at College Park, John Reppy University of Chicago, Olin Shivers Northeastern University, Skye Soss University of Chicago, Byron Zhong University of Chicago DOI | ||
11:15 25mTalk | Multiple Resumptions and Local Mutable State, Directly ICFP Papers Serkan Muhcu Technische Universität Berlin, Philipp Schuster University of Tübingen, Michel Steuwer Technische Universität Berlin, Jonathan Immanuel Brachthäuser University of Tübingen DOI | ||
11:40 25mPaper | OCaml Blockly JFP First Papers Kenichi Asai Ochanomizu University DOI | ||
13:40 - 15:20 | |||
13:40 25mTalk | Call-Guarded Abstract Definitional InterpretersDistinguished Paper ICFP Papers Kimball Germane Brigham Young University DOI | ||
14:05 25mTalk | Effectful Lenses: There and Back with Different MonadsDistinguished Paper ICFP Papers DOI | ||
14:30 25mTalk | First-Order LazinessDistinguished Paper ICFP Papers Anton Lorenzen University of Edinburgh, Daan Leijen Microsoft Research, Wouter Swierstra Utrecht University, Netherlands, Sam Lindley The University of Edinburgh DOI Pre-print | ||
14:55 25mTalk | Multi-stage Programming with Splice VariablesDistinguished Paper ICFP Papers DOI | ||
16:00 - 17:40 | |||
16:00 25mTalk | Pushing the Information-Theoretic Limits of Random Access Lists ICFP Papers Edward Peters , Yong Qi Foo National University of Singapore, Michael D. Adams National University of Singapore DOI | ||
16:25 25mTalk | Truly Functional Solutions to the Longest Uptrend Problem (Functional Pearl) ICFP Papers DOI | ||
16:50 25mPaper | Bottom-up computation using trees of sublists JFP First Papers Shin-Cheng Mu Academia Sinica, Taiwan DOI | ||
17:15 25mPaper | You could have invented Fenwick trees JFP First Papers Brent Yorgey Hendrix College DOI | ||
16:00 - 17:40 | |||
16:00 25mPaper | A contextual formalization of structural coinduction JFP First Papers DOI | ||
16:25 25mPaper | A practical formalization of monadic equational reasoning in dependent-type theory JFP First Papers Reynald Affeldt National Institute of Advanced Industrial Science and Technology (AIST), Japan, Jacques Garrigue , Takafumi Saikawa Nagoya University DOI | ||
16:50 25mTalk | Almost Fair Simulations ICFP Papers Arthur Correnson CISPA Helmholtz Center for Information Security, Iona Kuhn Saarland University, Bernd Finkbeiner CISPA Helmholtz Center for Information Security DOI | ||
17:15 25mTalk | Big Steps in Higher-Order Mathematical Operational Semantics ICFP Papers Sergey Goncharov University of Birmingham, Pouya Partow Birmingham University, Stelios Tsampas University of Southern Denmark DOI | ||
Tue 14 OctDisplayed time zone: Perth change
Tue 14 Oct
Displayed time zone: Perth change
10:50 - 12:05 | |||
10:50 25mTalk | Robust Dynamic Embedding for Gradual Typing ICFP Papers Koen Jacobs Inria, Matías Toro University of Chile, Nicolas Tabareau Inria, Éric Tanter University of Chile DOI | ||
11:15 25mPaper | A simple blame calculus for explicit nulls JFP First Papers DOI | ||
11:40 25mTalk | SecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F* ICFP Papers Cezar-Constantin Andrici MPI-SP, Danel Ahman University of Ljubljana, Cătălin Hriţcu MPI-SP, Ruxandra Icleanu University of Edinburgh, Guido Martínez Microsoft Research, Exequiel Rivas Tallinn University of Technology; Ahrefs, Théo Winterhalter INRIA DOI | ||
10:50 - 12:05 | |||
10:50 25mTalk | Compiling with Generating Functions ICFP Papers DOI | ||
11:15 25mTalk | Correctness Meets Performance: From Agda to Futhark ICFP Papers DOI | ||
11:40 25mPaper | Domain-specific tensor languages JFP First Papers Jean-Philippe Bernardy University of Gothenburg, Sweden, Patrik Jansson Chalmers University of Technology and University of Gothenbrug DOI | ||
13:40 - 15:20 | |||
13:40 25mTalk | Fulls Seldom Differ ICFP Papers Mark Koch Quantinuum, Alan Lawrence Quantinuum, Conor McBride University of Strathclyde, Craig Roy Quantinuum DOI | ||
14:05 25mTalk | Normalization by Evaluation for Non-cumulativity ICFP Papers Shengyi Jiang The University of Hong Kong, Jason Z. S. Hu Amazon, Bruno C. d. S. Oliveira University of Hong Kong DOI | ||
14:30 25mTalk | Type Theory in Type Theory using a Strictified Syntax ICFP Papers DOI Pre-print | ||
14:55 25mTalk | Type Universes as Kripke Worlds ICFP Papers Paulette Koronkevich University of British Columbia, William J. Bowman University of British Columbia DOI Pre-print | ||
13:40 - 15:25 | |||
13:40 25mTalk | A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Quantum Hardware ICFP Papers Liyi Li Iowa State University, David Young University of Kansas, USA, James Bryan Graves Indiana University, Chandeepa Dissanayake Iowa State University, Amr Sabry Indiana University DOI | ||
14:05 25mTalk | Functional Networking for Millions of Docker Desktops (Experience Report) ICFP Papers Anil Madhavapeddy University of Cambridge, UK, David J. Scott Docker, Inc., Patrick Ferris University of Cambridge, UK, Ryan Gibb University of Cambridge, Thomas Gazagnaire Tarides DOI | ||
14:30 25mTalk | Polynomial-Time Program Equivalence for Machine Knitting ICFP Papers Nathan Hurtig University of Washington, Jenny Han Lin University of Utah, Thomas S. Price Carnegie Mellon University, Adriana Schulz University of Washington, James McCann Carnegie Mellon University, Gilbert Bernstein University of Washington DOI | ||
14:55 30mTalk | SRC Talks ICFP Student Research Competition | ||
16:00 - 18:00 | |||
16:00 30mTalk | ICFP Contest Report ICFP Papers | ||
16:30 15mAwards | Award Ceremony ICFP Papers | ||
16:45 5mAwards | SRC Awards ICFP Student Research Competition | ||
16:50 15mMeeting | PC Chair Report ICFP Papers | ||
17:05 10mTalk | General Chair Report ICFP Papers | ||
17:15 10mTalk | ICFP 2026 Announcement ICFP Papers Sam Tobin-Hochstadt Indiana University | ||
Wed 15 OctDisplayed time zone: Perth change
Wed 15 Oct
Displayed time zone: Perth change
10:50 - 12:05 | |||
10:50 25mTalk | A Bargain for Mergesorts: How to Prove Your Mergesort Correct and Stable, Almost for Free ICFP Papers Cyril Cohen Inria - CNRS - ENS Lyon - Université Claude Bernard Lyon 1 - LIP - UMR 5668, Kazuhiko Sakaguchi CNRS - ENS Lyon - Université Claude Bernard Lyon 1 - LIP - UMR 5668 DOI Pre-print | ||
11:15 25mTalk | CRDT Emulation, Simulation, and Representation Independence ICFP Papers Nathan Liittschwager University of California, Santa Cruz, Jonathan Castello University of California, Santa Cruz, Stelios Tsampas University of Southern Denmark, Lindsey Kuper University of California, Santa Cruz DOI Pre-print | ||
11:40 25mPaper | How much is in a square? Calculating functional programs with squares JFP First Papers Jose Nuno Oliveira University of Minho; INESC TEC DOI | ||
10:50 - 12:05 | |||
10:50 25mTalk | Fusing Session-Typed Concurrent Programming into Functional Programming ICFP Papers Chuta Sano McGill University, Deepak Garg MPI-SWS, Ryan Kavanagh Université du Québec à Montréal, Brigitte Pientka McGill University, Bernardo Toninho Instituto Superior Técnico - University of Lisbon DOI | ||
11:15 25mTalk | Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs ICFP Papers Kwing Hei Li Aarhus University, Alejandro Aguirre Aarhus University, Simon Oddershede Gregersen New York University, Philipp G. Haselwarter Aarhus University, Joseph Tassarotti New York University, Lars Birkedal Aarhus University DOI Pre-print | ||
11:40 25mTalk | Relax! The Semilenient Core of Choreographic Programming (Functional Pearl) ICFP Papers Dan Plyukhin University of Southern Denmark, Xueying Qin University of Southern Denmark, Fabrizio Montesi University of Southern Denmark DOI Pre-print | ||
13:40 - 15:20 | |||
13:40 25mTalk | Formal Semantics and Program Logics for a Fragment of OCaml ICFP Papers DOI | ||
14:05 25mTalk | Verified Interpreters for Dynamic Languages with Applications to the Nix Expression Language ICFP Papers DOI Pre-print | ||
14:30 25mTalk | Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach ICFP Papers Marcos Grandury IMDEA Software Institute; Universidad Politécnica de Madrid, Aleksandar Nanevski IMDEA Software Institute, Alexander Gryzlov IMDEA Software Institute DOI | ||
14:55 25mTalk | Reasoning about Weak Isolation Levels in Separation Logic ICFP Papers Anders Alnor Mathiasen Aarhus University, Léon Gondelman Aalborg University, Léon Ducruet Aarhus University, Amin Timany Aarhus University, Lars Birkedal Aarhus University DOI | ||
13:40 - 15:20 | |||
13:40 25mTalk | McTT: A Verified Kernel for a Proof Assistant ICFP Papers Junyoung Jang McGill University, Antoine Gaulin McGill University, Jason Z. S. Hu Amazon, Brigitte Pientka McGill University DOI Media Attached | ||
14:05 25mTalk | Linear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl) ICFP Papers Maximilian Doré University of Oxford DOI Pre-print | ||
14:30 25mPaper | Binary search—think positive JFP First Papers DOI | ||
14:55 25mTalk | Teaching Software Specification (Experience Report) ICFP Papers DOI | ||