The Dutch Functional Programming Day (also known as the FP Dag) is an annual gathering of researchers, students, and practitioners sharing a common interest in functional programming. The day features talks that cover the latest advances in research, teaching, and applications in functional programming in the broadest sense. Coffee and lunch breaks provide ample opportunity for networking with your colleagues and meeting new people. Experts and newcomers to the field are equally welcome.

We welcome all FP enthusiasts from the Netherlands, Belgium, and other neighbouring countries. The language of the FP Day is English.

When and Where

The FP Dag takes place on Friday, January 9, 2026. The presentations will take place in room HG 00.616 of the Huygensgebouw, Heyendaalseweg 135, 6525AJ Nijmegen, The Netherlands; lunch will be provided in the neighbouring Mercatorgebouw. For public transport, see the aforementioned website of the Huygensgebouw. For parking, we recommend using the car park at Toernooiveld or the car park underneath the Huygens building (no longer closed).

Schedule

Talk Abstracts

A Genealogy Functional Programming
Philip Kaludercic

In a critical contribution to the futile endeavor to agree what "functional programming" even is supposed to be, I will be sketching the background, conditions, implementations and development of features commonly associated with functional programming (recursion, pure and first-class functions/higher-order functions, ADTs, absence of side-effects, lazy evaluation, ...).

FuPy – A Python library for Functional Programming
Tom Verhoeff

One view on FuPy is that it is a DSL (for functional programming) embedded in Python. Another view is that it adds very basic features missing in standard Python to do functional programming properly.

Python does support functions as (almost) first-class citizens in that they can be arguments to and results of functions (some call these higher-order functions). But Python lacks a predefined identity function and function composition.

My presentation will motivate the introduction of FuPy, give some examples, provide some insights into its design, and reflect on lessons learned.

SaC, an alternative to Python for the performance critical part of novel ML approaches?
Sven-Bodo Scholz

TBD

Intrinsically Recursive Coalgebras
Cass Alexandru

When it comes to structured recursion, recursive coalgebras are one of, if not the fundamental notion. However, proving recursivity of a given coalgebra has so far been cumbersome and alien to the process of total functional programming in dependently typed languages. We (joint work with Henning Urbat & Thorsten Wißmann) present a new sufficient criterion for all coalgebras for a functor on type families over the carrier of a well-founded relation to be recursive, which is amenable to formalisation, and apply it to example algorithms.

Symmetries in Sorting
Wind Wong

Sorting algorithms are fundamental to computer science, and their correctness criteria are well understood as rearranging elements of a list according to a specified total order on the underlying set of elements. As mathematical functions, they are functions on lists that perform combinatorial operations on the representation of the input list. In this paper, we study sorting algorithms conceptually as abstract sorting functions.

There is a canonical surjection from the free monoid on a set (lists of elements) to the free commutative monoid on the same set (multisets of elements). We show that sorting functions determine a section (right inverse) to this surjection satisfying two axioms, that do not presuppose a total order on the underlying set. Then, we establish an equivalence between (decidable) total orders on the underlying set and correct sorting functions.

The first part of the paper develops concepts from universal algebra from the point of view of functorial signatures, and gives constructions of free monoids and free commutative monoids in (univalent) type theory. Using these constructions, the second part of the paper develops the axiomatisation of sorting functions. The paper uses informal mathematical language, and comes with an accompanying formalisation in Cubical Agda.

Lightweight Formalisation of Denotational Semantics in Agda
Peter Mosses

We postulate an Agda type of Scott-domains, together with various domain constructors. The carriers of domains have bottom elements, and domains of endofunctions have a fixed-point operator. Recursive domain definitions are supported by postulating bijections between domains. After rewriting the carrier types of function domains to ordinary function types, definitions in λ-notation can be embedded almost verbatim in Agda.

This approach has been used to give a lightweight formalisation of a denotational semantics of the Scheme programming language. The Agda type-checker reported several errors in the formalisation, and all of them corresponded to errors in the original semantics.

Reasoning About Amortized Cost: From Syntax to Semantics
David Binder

When we verify the correctness of functional data structures and algorithms, it is not sufficient to just verify functional correctness; we also have to verify non-functional properties such as algorithmic complexity. Ideally, we want to do this with the tools that functional programmers are already familiar with, i.e. in the types of the functions themselves.

In this talk I am going to present one such type system which is powerful enough to encode the reasoning principles that we use when we analyse the amortized complexity of algorithms: the system “lambda-amor” introduced by V. Rajani, M. Gaboardi, D. Garg and J. Hoffmann. But if we want to prove that this type-based analysis is sound we have to go from its syntax to its semantics: In the second part of the talk, I will present a novel categorical semantics of amortized cost analysis in terms of an adjunction between “graded cost” and “graded potential”.

The talk is designed to be accessible to a wide audience and will be example-driven. I will start with a simple informal amortized analysis of queues, and introduce the type-theoretic tools like graded monads step-by-step. Only at the very end will I give a short outlook on the denotational semantics of the type theory in terms of adjunctions that we developed.

(This talk presents joint work with Dominic Orchard, Vineet Rajani and David Corfield.)

Smart With
Nathaniel Burke

The "with construct", proposed by McBride and McKinna in "The view from the left" (2004), extends pattern matching in dependently-typed languages with a mechanism for matching on intermediary computations (similar to "case expressions", ubiquitous in functional programming languages with simpler type systems).

This construct is implemented in Agda under the name "with-abstractions" and, while useful, the feature can also be a footgun. Proving simple laws about definitions by with-abstraction is often fiddly and sometimes impossible due to "ill-typed with-abstraction" errors.

In this talk, I will present some ongoing work on an improved "with-abstraction" mechanism for Agda, inspired by the "smart case" proposal of Altenkirch et al. I will discuss some of the difficulties involved in retaining decidable typechecking.

Liberating functional programming from the message passing style
Adriaan Leijnse

Impure effects like send and receive make it hard to compose distributed programs like we compose purely functional ones. Even in small examples issueswith ordering and consistency can leak through.

In this talk I'll present a different way of thinking about distributed programs: a composable semantics that lets us to write them in a just values and functions style, without relying on effects. Liberated from message passing, we'll explore how this change of perspective might help us reach new levels of abstraction in distributed programming.

SaC, an alternative to Python for the performance critical part of novel ML approaches?
Sven-Bodo Scholz

Python has taken center stage when it comes to implementing ML algorithms. The languages convinces through its flexibility and the availability of many libraries. Libraries such as NumPy or CuPy ultimately enable very good performance which helps bridging the gap between Python's flexibility and the sophisticated parallel code needed for performance.

In this talk, we make the case for Single Assignment C (SaC) as an alternative for computational kernels where performance across a wide range of parallel architectures is needed but no highly tuned libraries are available yet. In contrast to Python, SaC focusses on arrays as main data structure, builds on a type system that is aware of array shapes, and generates high-performance codes for multi-core machine, GPUs and clusters alike. As it turns out, rank-polymorphism, a key feature of SaC, does not only allow for more generic programs but, surprisingly, it also helps when optimising across different parallel platforms.

Dinner

We will end the day with a joint dinner at De Hemel, Franseplaats 1, 6511 VS Nijmegen at 18 o'clock. The dinner is at your own expense and requires pre-booking.

Registration

Registration is closed

Contact

Chair: Mart Lubbers
Website Chair: Benedikt Rips

Sponsors

This event is sponsored by:

TOP Software

Previous editions

2026: Radboud Universiteit, Nijmegen
2025: Katholieke Universiteit Leuven
2024: Technische Universiteit Delft
2023: Sioux Labs and Technische Universiteit Eindhoven
2022: Universiteit Utrecht
2021: none (COVID)
2020: Universiteit van Amsterdam
2019: Netherlands Defense Academy, Breda
2018: Belastingsdienst, Apeldoorn
2017: Radboud Universiteit, Nijmegen
2016: Universiteit Utrecht
2015: Universiteit van Twente
2014: Universiteit van Amsterdam
2013: Radboud Universiteit, Nijmegen
2012: Universiteit Utrecht
2011: Universiteit Twente, Enschede
2010: Radboud Universiteit, Nijmegen
2009: Technische Universiteit Eindhoven
2008: Open Universiteit, Utrecht
2007: Marine, Amsterdam
2006: Hogeschool Avans, Breda
2005: Rijksuniversiteit Groningen
2004: Universiteit Twente, Enschede
2003: Universiteit Utrecht
2002: Katholieke Universiteit Nijmegen
2001: Technische Universiteit Delft
2000: Technische Universiteit Eindhoven
1999: Hogeschool Breda
1998: Rijksuniversiteit Leiden
1997: Hogeschool Leeuwarden
1996: Universiteit van Amsterdam
1995: Technische Universiteit Twente, Enschede
1994: Rijksuniversiteit Utrecht
1993: Katholieke Universiteit Nijmegen