Description

The symposium on Trends in Functional Programming (TFP) is an international forum for researchers with interests in all aspects of functional programming, taking a broad view of current and future trends in the area. It aspires to be a lively environment for presenting the latest research results, and other contributions. See the call for papers for more details.

In 2025, the event is taking place in person in the Department of Computer Science at the University of Oxford. It will be a 4-day event, with TFPiE taking place on 13th January 2025, followed by TFP on 14th to 16th January.

TFP offers a friendly and constructive reviewing process designed to help less experienced authors succeed, with an opportunity for two rounds of review, both before and after the symposium itself. Authors thus have an opportunity to address reviewers’ concerns before the final decision on publication in the Proceedings is taken, in the light of previous reviews and discussions at the symposium.

TFP offers two “best paper” awards, the John McCarthy award for best paper, and the David Turner award for best student paper.

See the call for papers for details.

Registration

The early registration deadline will be 18th 20th December 2024, late registration 6th January 2025. For details, see the registration page.

Keynotes

Nicolas Wu, Imperial College London (TFPiE keynote)

Fractal Foundations and Galactic Graphs: Structure and Strategy for Expanding Minds

Computer science is rich in its applications, from the beautiful patterns found in fractals to the stragic problem-solving of graph algorithms. In this talk, we look at how coursework built around fractals and graphs has been used to help students understand core computer science material while keeping them inspired and engaged.

Bio: Nicolas Wu is a Reader of Computing at Imperial College London, where he leads the Functional Programming research group. His research focuses on programming languages, particularly the application of category theory to program semantics and algorithms. His recent work explores connections between domain-specific languages, algebraic effect handlers, and recursion schemes.

Graham Nelson, University of Oxford

Literate Programming and Cultural Practice

Literate programming, a dogma and doctrine in which commentary, reasoning and justification is mingled with code, got its distressingly in-your-face name at a time of gentle tussles for dominance among the Old Masters of computer science education: Donald Knuth, Edsger Dijkstra, Nicklaus Wirth, Christopher Strachey, and Tony Hoare. Literate programming can be seen as a radical, fresh manifesto very much of that era, a clarion call for a new hybrid literary form; or, as an attempt to look backwards, to encourage computer scientists to adopt stylistics of mathematical writing already two hundred years old. It can be seen as a humanist, as opposed to mechanistic, answer to a moral panic about program correctness, and the spectre of mass deaths from nuclear accidents and technological breakdown. Today, a generous verdict might be that LP was a brave idea which just didn’t scale. An ungenerous one, that it was never more than a page layout strategy for textbooks. Either way, though a handful of romantics do continue to use LP, it has passed into history as a cultural by-way, a road not taken. And yet: its real motivations go back to the age of flow-charts, have never gone away, and continue to be felt in the languages, package managers and development tools of the 2020s. LP made heavy use of macros and preprocessing, juvenile techniques (some say) which should have been thrown out with the last PDP-10: but, consider the sudden respectability of macros in production languages like Rust and Swift. LP mixed code with text, which (some say) is clumsy, verbose and misleading: but, consider the far-reaching consequences of Github’s decision to privilege Markdown files in its rendering of programs as websites, and how that has changed the way professionals present their work. My own view is that language designers, tool-chain authors and coding evangelists might benefit from a second, or even a first, look at literate programming. For all its faults it was a bid to make a practical study of one of the hardest coding questions of all: how are we to communicate and share our sprawling, broken, incomplete programs, with their half-articulated intentions always a shadowy presence behind them?

Bio: Graham Nelson is a Fellow in Mathematics at St Anne’s College of the University of Oxford, is the managing editor for the Modern Humanities Research Association, and is the author of Inform, a programming language for interactive fiction which is widely used by writers in and out of the games industry. The source code for Inform is one of the largest literate programs in the world.

Mike Sperber, Active Group

Things We Never Told Anyone About Functional Programming

FP—what is it good for? The “P” is for “Programming”, the writing of programs. Judging from the papers and most books on functional programming, FP excels as a tool for writing short programs—up to a hundred lines maybe. We also know that there are large FP codebases at large companies, and folklore has it that this also works quite well. Yet there is precious little literature on how to go from a hundred lines to a million lines of functional code. This hinders FP adoption by not-(yet?)-practicioners, who ask questions like:

Successful practitioners rely on folklore and experience for the answers to these questions, but precious little is written down in findable places and accessible formats.

This talk is a call to action: We need to do a better job at outreach—find the gaps in our published knowledge, write down what’s undocument and—going to extremes—talk to other communities who know a thing or two about large-scale software development.

Bio: Mike Sperber is CEO of Active Group, a software consultancy in Tübingen, Germany that develops software for client projects using functional programming. He has a long history of publishing on functional programming, including many research papers, and was the project editor for the R6RS standard for the Scheme programming language. He has also developed an introductory course in programming in use at several German universities, based on the PLT group’s Program by Design approach. He also co-authored (with Nicole Rauch and Lars Hupel) the curriculum on Functional Software Architecture for iSAQB.

Kathrin Stark, Heriot-Watt University

A Verified Foreign Function Interface Between Coq and C

One can write dependently typed functional programs in Coq, and prove them correct in Coq; one can write low-level programs in C, and prove them correct with a C verification tool. In this talk, I will present the Verified Foreign Function Interface (VeriFFI) and demonstrate how to write programs partly in Coq and partly in C, and interface the proofs together. VeriFFI then guarantees type safety and correctness of the combined program. It works by translating Coq function types (and constructor types) along with Coq functional models into VST function-specifications; if the user can prove in VST that the C functions satisfy those specs, then the C functions behave according to the user-specified functional models (even though the C implementation might be very different) and the proofs of Coq functions that call the C code can rely on that behavior. VeriFFI is joined work with Andrew Appel and Joomy Korkut.

Bio: Kathrin Stark is an Assistant Professor of Computer Science at Heriot-Watt University. She completed her doctorate at Saarland University, focusing on developing proofs with interactive proof assistants like Coq. Her research aims to advance the construction of rigorous formal proofs while minimizing the associated overhead through principled approaches. As a Postdoctoral Presidential Research Fellow, she collaborated with Joomy Korkut and Andrew Appel to develop a verified foreign function interface between Coq and C.

Important Dates

Submission deadline (pre-symposium, full papers) Wed 13th Nov 2024 (AOE)
Submission deadline (pre-symposium draft papers) Wed 11th Dec 2024 (AOE)
Early registration Wed 18th Fri 20th Dec 2024
Late registration Mon 6th Jan 2025
TFPiE Workshop Mon 13th Jan 2025
TFP Symposium Tue 14th to Thu 16th Jan 2025
Submission deadline (post-symposium review) Wed 19th Feb 2025 (AOE)

Sponsors

Organizing Committee

Jeremy Gibbons University of Oxford, UK Programme Chair
Jason Hemann Seton Hall University, US Conference Chair
Peter Achten Radboud University Nijmegen, NL Publicity Chair
Marco T. Morazán Seton Hall University, US Steering Committee Chair

TFP history