Functionality from Structure
The eleventh workshop on Mathematically Structured Functional Programming is devoted to the derivation of functionality from structure. It is a celebration of the direct impact of Theoretical Computer Science on programs as we write them today. Modern programming languages, and in particular functional languages, support the direct expression of mathematical structures, equipping programmers with tools of remarkable power and abstraction. Where would Haskell be without monads? Functional reactive programming without arrows? Call-by-push-value without adjunctions? The list goes on. This workshop is a forum for researchers who seek to reflect mathematical phenomena in data and control.
MSFP 2026 will be held on Saturday 18th July 2026 in affiliation with FSCD 2026 at FLoC 2026 in Lisbon, Portugal.
The proceedings will be published in EPTCS, as in recent years.
Kenji Maillard, INRIA, France
Cristina Matache, University of Birmingham, UK
Jaro Reinders (Delft University of Technology), Casper Bach (University of Southern Denmark), Benedikt Ahrens (Delft University of Technology), Nicolas Wu (Imperial College London), Effects with Variable Binding (talk only)
Algebraic effects let programmers declare the syntax of operations which can be used to write and compose effectful programs. Such programs can be run by applying effect handlers that give programmers control over when and how many times to call continuations of operations. Embedding algebraic effects and handlers in an existing language provides a lightweight and powerful approach to programming with effects. Such embeddings typically use host language functions to represent continuations of programs. While host language functions offer an ergonomic interface for programming with and handling effects, they also hinder programmers wishing to define custom optimizations for effectful programs. Specifically, optimizations that statically analyze and transform variable bindings cannot be defined, as that would require meta-programming facilities for host language functions. This paper presents a solution to this problem by embedding algebraic effects as intrinsically typed, De Bruijn-indexed syntax. Working in Agda, we demonstrate how this provides a safe-by-construction approach to programming with effects that is almost as ergonomic as the traditional embedding, but which additionally supports optimizations that inspect and transform variable binding.
Alexandre Garcia de Oliveira (Fatec Rubens Lara/Obsidian Systems), Free Semiarrows
This work studies semiarrows: profunctors that carry both a monoid structure under the Day convolution (parallel composition with unit) and a semigroup structure under profunctor composition (sequential composition without identity), linked by an interchange law and a unit interaction law. The term and definition were introduced in the author's doctoral thesis, generalising monoidal profunctors and arrows. We construct the free semiarrow over an arbitrary base profunctor~$p$, presented as a GADT |FreeSemi p| with five constructors corresponding to the semiarrow operations. We give the interpretation function |interpretSync|, which, given a natural transformation from~$p$ to any target semiarrow~$q$, produces the unique semiarrow homomorphism extending the natural transformation. As a running example we develop an arithmetic-circuit DSL over a prime field. Primitive gates form a GADT; |FreeSemi RelGate| is the resulting circuit term algebra for constraint checking. Because no |arr| combinator is available, every fan-out and structural routing must appear explicitly, making every circuit term inspectable. We present an interpretation of the R1CS cost model via |interpretSync|.
Niyousha Najmaei (École Polytechnique), Niels van der Weide (Radboud University), Benedikt Ahrens (Delft University of Technology), Paige Randall North (Utrecht University), A Type Theory for Comprehension Categories (talk only)
Recent models of intensional type theory have been constructed in algebraic weak factorization systems (AWFSs). AWFSs give rise to comprehension categories that feature non-trivial morphisms between types; these morphisms are not used in the standard interpretation of Martin-Löf type theory in comprehension categories. We develop a type theory that internalizes morphisms between types, reflecting this semantic feature back into syntax. Our type theory comes with Π-, Σ-, and identity types. We discuss how it can be viewed as an extension of Martin-Löf type theory with coercive subtyping, as sketched by Coraglia and Emmenegger, and we recognize this structure in many intensional models of Martin-Löf type theory. This talk is based on a recently published paper and its ongoing continuation.
Ohad Kammar (University of Edinburgh), Matija Pretnar (University of Ljubljana), Mathematical foundations for symmetric programming Composition (talk only)
We propose abstractions for exploiting symmetries in programming and reasoning based on the mathematical proof principle "without-loss-of-generality" (wlog). We decompose such arguments into three components. The first component makes the symmetry explicit by defining appropriate groups and their action on the input/assumptions and output/conclusions. The second component explicates how to canonise the input, by choosing appropriate symmetries for each input. The third component is a core function/proof that transforms canonical inputs into outputs. The proposed wlog construct combines these components: given an input, calculate its canonising symmetry, use the symmetry to canonise the input, apply the core function to the canonical input, and apply the inverse symmetry to the output. Here we develop the mathematical foundations for these abstractions. We illustrate the approach on running examples: sliding-tile merges in 2048, binary-tree insertion, and Schur's inequality as a mathematical instance of WLOG. We extend the framework to algebraic datatypes using initial algebra semantics, showing how a G-symmetry strength on a functor lifts group actions to inductive types and that the unique fold into an equivariant algebra is itself equivariant, allowing us to avoid using general recursion to define a symmetric version of tree insertion. Finally, we develop the theory of equivariant canonisers and explore the cases when the WLOG construction is guaranteed to produce an equivariant function.
Eigil Rischel (Tallinn University of Technology), Towards Minimal Axioms for Probabilistic Programming (talk only)
I will present a recent result giving a very simple characterization of the Giry monad on (standard Borel) measurable spaces in terms of a (initial) universal property. In addition, I'll present some ongoing work on adapting this result to categories more suited for functional programming, such as elementary toposes.
Aleksei Tiurin, Dan Ghica (University of Birmingham), Nick Hu (Kyoto University), Categorical E-Graphs for Lambda Calculi
Equality saturation is a powerful technique for program optimisation and reasoning, driven by the use of equivalence classes of terms under rewrite rules. These equivalence classes lie at the root of data structures called equality graphs (e-graphs). Despite their numerous advantages, until recently e-graphs lacked native support for variable binding, limiting their applicability to programming languages. We propose to address this problem from a categorical perspective by extending the interpretation of e-graphs as string diagrams, namely morphisms in symmetric monoidal semilattice-enriched categories which we additionally equip with a monoidal closed structure. We further define a concrete representation using hierarchical hypergraphs, and introduce a corresponding double-pushout (DPO) rewriting system. Finally, we establish the equivalence between term rewriting and DPO rewriting, with the combinatorial model inherently absorbing the equations of the symmetric monoidal structure. Our approach, specifically designed for lambda calculi, is compared and contrasted with slotted e-graphs --- an alternative method for incorporating variable binding within e-graphs.
Fiona Blackett, Vikraman Choudhury, Rin Liu (University of Strathclyde), Symmetric List Objects (talk only)
Cons-lists are fundamental to functional programming, and are well-understood as initial algebras, and as a concrete construction of free monoids. In category theory, such list objects can be axiomatised internal to any monoidal category, with nil and cons maps, and a recursion mechanism. When strengthened to support parametrised recursion, they can be shown to give the free monoid construction. We study a small variant on parametrised list objects called parametrised symmetric list objects, in a symmetric monoidal category, where the two frontmost elements are allowed to be permuted. We show that this gives a construction of free commutative monoids, and develop some related theory.
Bjarki Gunnarsson (University of Iceland), Exequiel Rivas (Tallinn University of Technology), Tarmo Uustalu (Reykjavik University and Tallinn University of Technology) Concurrent monads as monads in a 2-category (talk only)
We discuss the concurrent monads of Rivas and Jaskelioff, a structure axiomatizing effectful notions of computation supporting not only sequential, but also parallel composition. We have previously analyzed accessible concurrent monads on given monoidal ordered category as lax duoid objects in a certain duoidal ordered category. Here we explain the different perspective that concurrent are monads in a certain 2-category and what this entails.
Registration is via the FLoC registration website. The early registration deadline is 15th May (conferences and workshops) or 1st June (workshops only).
The programme will be published soon
Submissions are welcomed on, but not restricted to, topics such as:
Please contact the programme co-chairs Robert Atkey and Marie Kerjean if you have any questions about the scope of the workshop.
We accept two categories of submission:
References and appendices are not included in page limits, but reviewers may or may not read appendices. Accepted papers and talks must be presented at the workshop by at least one of the authors.
We are using FLoC HotCRP instance to manage submissions.
See the main MSFP page.