Skip to the content.

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 December 2024, late registration 6th January 2025. Further information to follow.

Keynotes

Nicolas Wu, Imperial College London (TFPiE keynote)

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.

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 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

To follow.

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