TFP 2025 – Schedule
All talks take place in the Bill Roscoe Lecture Theatre on the ground floor of the Wolfson Building, Department of Computer Science, University of Oxford.
Jump to the schedule for Monday / Tuesday / Wednesday / Thursday.
Monday 13th January
See the TFPiE schedule for details.
Tuesday 14th January
| 09:00–10:00 | Things We Never Told Anyone About Functional Programming Mike Sperber (Chair: Jeremy Gibbons) |
keynote |
| 10:00–10:25 | Time as a First-Class Citizen: The ∆Q Systems Design Project Kevin Hammond, Peter Thompson, Neil Davies, Peter van Roy, James Chapman, Heinrich Apfelmus, Hossein Haeri, Magne Haveraaen, Mikhail Barash, Artjoms Šinkarovs |
|
| 10:25–10:55 | coffee | |
| 10:55–12:10 | Exploring Female and Male Student Perceptions in a Functional-Programming-Based Automata Theory Course Marco Morazan, Tijana Minic, Andres Garced Using GHC Core to Normalise Student Programs Alex Gerdes, Matilda Blomqvist R7RS Large: Bringing Schemers (Back) Together for Scheme’s Fiftieth Birthday Daphne Preston-Kendal (Chair: Jason Hemann) |
|
| 12:10–14:00 | lunch | |
| 14:00–15:15 | Multi-GPU Code Generation for Out-Of-Core Problems Sven-Bodo Scholz, Thomas Koopman, Patrick van Beurden Shallowly Embedded Functions Mart Lubbers, Pieter Koopman, Niek Janssen KappaMutor: A Compact Structured Combinator Processor for Haskell Yukang Xie, Craig Ramsay, Robert Stewart, Hans-Wolfgang Loidl (Chair: Kevin Hammond) |
|
| 15:15–15:45 | tea | |
| 15:45–17:00 | A Formal Semantics for the Spreadsheet Core Enzo Alda, Daniel Andres Pinto Alvarado A Reflection on Task-Oriented Programming Mart Lubbers, Tim Steenvoorden Self-aware Program Analysis in stableKanren Xiangyu Guo, Ajay Bansal (online) (Chair: Sven-Bodo Scholz) |
Wednesday 15th January
| 09:00–10:00 | Literate Programming and Cultural Practice Graham Nelson (Chair: Paul Downen) |
keynote |
| 10:00–10:25 | Towards a Theory of Type-Safe Renaming and Refactoring Casper Bach, Luka Miljak, Rosilde Corvino |
|
| 10:25–10:55 | coffee | |
| 10:55–12:10 | Heapless Functional Programming Ellis Kesterton, Edwin Brady Reconstructing Big-Step Continuation-Passing Semantics for WebAssembly Guannan Wei, Alexander Bai, Dinghong Zhong, Jiatai Zhang Explicit Level Imports Matthew Pickering, Rodrigo Mesquita, Adam Gundry (Chair: Pedro Vasconcelos) |
|
| 12:10–13:50 | lunch | |
| 13:50–15:30 | Checking the Unchecked: Demonstrating Correct Behaviour of the Cardano Blockchain node using Lightweight Formal Methods Kevin Hammond, Ulf Norell, Maximilian Algehad, James Chapman, Thomas Arts Formal Specification and Functional Programming Implementation of Distributed Lazy Group Membership Protocol Jianhao Li, Viktoria Zsok Energy-Aware Dynamic Adaptation of Runtime Systems Jordy Aaldering, Bernard van Gastel, Sven-Bodo Scholz Communication for Task-Oriented Systems with Edge Devices Niek Janssen, Pieter Koopman, Mart Lubbers (Chair: Guannan Wei) |
|
| 15:30–18:30 | excursion | |
| 19:00–21:30 | banquet |
Thursday 16th January
| 09:00–10:00 | A Verified Foreign Function Interface Between Coq and C Kathrin Stark (Chair: Casper Bach) |
keynote |
| 10:00–10:25 | CoScheme: Compositional Copatterns in Scheme Paul Downen, Adriano Corbelino II |
|
| 10:25–10:55 | coffee | |
| 10:55–12:10 | Functional Reactive GUI Programming with Modal Types Jean-Claude Disch, Asger Heegaar, Patrick Bahr Noninterference through Bisimulation Alex Kavvos, Wendy Yang, April Tune Quantifiers for Quantitative Logics in Coq: a New Project Description Jairo Miguel Marulanda Giraldo, Ekaterina Komendantskaya, Alessandro Bruni, Reynald Affeldt, Matteo Capucci (Chair: Martin Lester) |
|
| 12:10–14:00 | lunch | |
| 14:00–15:15 | Context-free Languages, Type Theoretically Jaro Reinders Custom Representations of Inductive Families Constantine Theocharis, Edwin Brady Two Dimensional Numerical Representations An Adventure with Block Matrices Michael Youssef (online) (Chair: Wouter Swierstra) |
|
| 15:15–15:45 | tea | |
| 15:45–17:00 | Synthesizing Accumulative Functions via Program Transformation Junyu Lin, Akimasa Morihata Alpha-Beta Pruning with the Selection Monad Johannes Hartmann On the Correctness of Barron and Strachey’s Cartesian Product Function Wouter Swierstra, Jason Hemann (Chair: Viktoria Zsok) |
Here is a zip file of all the accepted submissions.