Title: Program Semantics with Interaction Trees
Advisor: Thomas Somers
Chair: Ties Steijn
Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic, Interaction trees: representing recursive and impure programs in Coq, Proc. ACM Program. Lang. 4, POPL, Article 51 (January 2020), 32 pages. 2019.
Max Vistrup, Michael Sammler, and Ralf Jung, Program Logics à la Carte, Proc. ACM Program. Lang. 9, POPL, Article 11 (January 2025), 32 pages. 2025.
Abstract:
There are three broad approaches to program semantics: Operational semantics, which define the execution of a program;
denotational semantics, which describes a program as a mathmatical object; and program logics, which uses logical rules to describe properties about programs.
Interaction Trees (ITrees) are a denotational semantics that is capable of denoting effectful, recursive and diverging programs. The main benefit of this approach over the traditional operational semantics models is that it is modular and allows for equational reasoning. Extensions to languages can thus easily be accommodated aswell as reasoning about program equivalence. Through effect interpretation, ITrees additionally has a notion of execution.
The modularity of Interaction trees lends itself well to be used in the domain of programming logics. Traditionally programming logics are defined by formulating logical rules and a soundness proof w.r.t an operational semantic model. Instread ITrees can be used as the underlying semantic model, which allows for reusable and extendable program logic fragments.
Title: Session Types with Classical and Intuitionistic Logic
Advisor: Simcha van Collem
Chair: Sonia
Philip Wadler, Propositions as Sessions, The 17th ACM SIGPLAN International Conference on Functional Programming. ICFP 2012.
Bas van den Heuvel and Jorge A. Pérez, Session Type Systems based on Linear Logic: Classical versus Intuitionistic, 12th International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software, Electronic Proceedings in Theoretical Computer Science (EPTCS), Vol. 314. 2020.
Abstract:
Most software systems contain many components that run concurrently. These components, or more precisely, processes, often communicate with each other. The λ-calculus is a minimal and very powerful model of computation, but it focuses on single sequential processes. The π-calculus plays a similar role for concurrent processes. Instead of the evaluation of functions, it supports the communication between processes, which is achieved through channels. If one process sends a message on such a channel, some other process should receive it on the same channel, and this communication is private to the two processes involved.
In the λ-calculus, types are used to reason about the kind of data in a program. In the same way, session types are used to reason about the protocol of a channel. A session type could describe this protocol: "First the client sends a request, then the server replies, and then the connection closes." Similar to how types come from traditional logic via the Curry-Howard correspondence, session types come from linear logic. Linear logic treats assumptions as resources: they should be used exactly once. This naturally fits concurrent processes. A process communicating via some channel according to some protocol is expected to follow it exactly once on that channel.
One desirable property of a concurrent program is locality. It means that if a process receives a channel, it may use that channel to send messages, but not to receive messages. As a consequence, each channel has exactly one receiving process, so it is always clear which process is responsible for handling an incoming message. The π-calculus based on classical linear logic (πCLL) does not enforce locality, while the π-calculus based on intuitionistic linear logic (πILL) does. The first paper by Wadler discusses the π-calculus based on classical logic, and the second paper by van den Heuvel and Pérez defines a π-calculus based on united linear logic (πULL), a logic that can be used classically and intuitionistically.
Title: Reasoning about Probabilistic Programs using Coalgebra
Advisor: Lukas Mulder
Chair: Kati Overbeeke
Wojciech Różowski and Alexandra Silva, A Completeness Theorem for Probabilistic Regular Expressions, In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '24). Association for Computing Machinery, New York, NY, USA, Article 66, 1–14. 2024.
J.J.M.M. Rutten, Universal coalgebra: a theory of systems, Theoretical Computer Science, Volume 249, Issue 1, 2000, Pages 3-80, ISSN 0304-3975. 2000.
Abstract:
How to prove that two probabilistic imperative programs are the same? The first paper defines a reasoning system to prove equivalence syntactically, for a simplified class of programs called Probabilistic Regular Expressions (PRE). We can trust the system because they prove it is sound and complete with respect to the model of probabilistic languages. They also show that each PRE corresponds to a unique Generative Probabilistic Transition System (GPTS), which is the probabilistic analogue of Kleene's theorem (every regular expression corresponds to a unique deterministic finite automaton).
In this talk, I will build up the necessary concepts before analysing the soundness and completeness proofs. I will first mention well-known results about the usual Regular Expressions, to understand what is missing in the probabilistic case. To fill the gaps, I will present PRE and GPTS, an operational and a denotational semantics for PRE, and the system for proving PRE equivalence. Then, I will sketch the soundness and completeness proofs, introducing the required coalgebraic concepts along the way using the second paper above. The goal is to see why coalgebra is important here: it abstracts away tedious details, so we can easily reuse recent results and others can reuse ours.
Title: Approximating polynomial roots by counting, and the Geode
Advisor: Wieb Bosma
Chair: Thomas Posthuma
N. J. Wildberger and Dean Rubine, A Hyper-Catalan Series Solution to Polynomial Equations, and the Geode, The American Mathematical Monthly Volume 132, Issue 5. 2025.
Ira M. Gessel, Lattice Paths and the Geode, arXiv preprint. 17 Jul 2025.
Abstract:
The Catalan numbers are an integer sequence with many combinatorial interpretations. "Triagons" are one of them – Wildberger and Rubine show that their structure gives a root for quadratic polynomials. This argument is generalized to "subdigons", which give a root for polynomials of any degree. The resulting series doesn't always converge, but by using a bootstrapping method we can approximate all (complex) roots of a polynomial.
In their investigation, a previously undocumented sequence emerges: the Geode. What does it count? By switching from "subdigons" to "lattice paths", Gessel proves an intuitive interpretation for the Geode.
Title: Negative translations and their use in classical realizability
Advisor: Niels van der Weide
Chair: Ben van Wijngaarden
Gilda Ferreira and Paulo Oliva, On the Relation Between Various Negative Translations, Logic, Construction, Computation. 2012.
Paulo Oliva and Thomas Streicher, On Krivine's realizability interpretation of classical second-order arithmetic, Fundamenta Informaticae. 2008.
Abstract:
Realizability is a technique used in logic that can be used to interpret arithmetic in the lambda-calculus, giving us a 'witness' of arithmetical formulas that are true in our logic. This is usually done in the context of intuitionistic logic, but can also be extended to classical logic.
One of the papers studies Krivine's realizability interpretation of classical second-order arithmetic, showing that Krivine's classical realizability can be split into a negative translation followed by an intuitionistic realizability step. The negative translation is the key part allowing us to extend realizability to classical logic. It turns classically valid formulas into intuitionistically valid formulas.
There are various negative translations that could be used, some simpler than others. The other paper makes this precise, giving a notion of what it means for one (modular) negative translation to be simpler than another, and thereby inducing a partial order on (modular) negative translations with respect to which some of the more common negative translations are minimal elements.
Title: Effectful realizability
Advisor: Niels van der Weide
Chair: Floris Reuvers
L. Cohen, A. Grunfeld, D. Kirst and E. Miquey, Syntactic Effectful Realizability in Higher-Order Logic. 2025.
L. Cohen, E. Miquey and R. Tate, Evidenced Frames: A Unifying Framework Broadening Realizability Models. 2021.
Abstract:
We introduce two kinds of realizability models that allow for
effectful computation, and show how they relate to each other and to the more
standard model of triposes.
The first model is EffHOL, an effectful form of HOL that also provides an effectful language that is essentially the same as Fω, but with a monadic computation type to allow for effects. HOL theorems and proofs can then be translated to types and programs respectively, where the program will satisfy a specification that can also be obtained from the theorem.
The second model is an evidenced frame, that uses an effectful form of a PCA called a computational system. Propositions are realized as sets of terms in the computational system, and entailment is realized by a term that transforms terms for one proposition into those of another. We show that for many interpretations of the monad in EffHOL, we may construct an evidenced frame.
Finally, a tripos is a model of HOL based on category theory, where basic propositional logic is implemented via Heyting algebras, and predicate logic is implemented via a functor Set^op → HA. Quantifiers are then implemented as adjoints, and higher-order reasoning is achieved via the existence of a generic predicate that allows the interpretation of propositions as terms. Finally, we show how any evidenced frame induces a tripos.
Title: Theorem & Proofs For Free!
Advisor: Bálint Kocsis
Chair: Codrin Iftode
Philip Wadler, Theorems for free, FPCA '89: Proceedings of the fourth international conference on Functional programming languages and computer architecture. 1989.
Bernardy, Jansson, Paterson, Proofs for free: Parametricity for dependent types, Cambridge University Press. 2012.
Abstract:
We will discuss Philip Wadler's 1989 paper 'Theorems for Free' paired with 'Proofs for Free' from 2012. The main topic will be parametricity, System F, Pure Type Systems and the Curry-Howard correspondence.
In Wadler's paper, we explore parametricity in a naive-set theoretic notation, and how it relies on System F's polymorphism. Wadler's main thesis was expanding on Reynold's ideas by showing how to derive theorems for free, meaning deriving theorems for functions that comes only from their type. We will also see an example of how to derive such a theorem for the type 'Rearrangement' ∀X.X* → X*
The second paper goes beyond System F and explores parametricity in the generalized Pure Type Systems. We will cover the Curry-Howard correspondence and how to derive Proofs For Free by viewing one Pure Type System as the programming language and another Pure Type System as the proof language where parametricity holds.
Title: State identification using characterizing sets or separating sequences
Advisor: Loes Kruger
Chair: Erin Leachman
U. Türker, R. Hierons, M. R. Mousavi and K. El-Fakih, Efficient state identification for finite state machine-based testing, IEEE Transactions on Software Engineering (expected). 2025.
Rick Smetsers, Joshua Moerman, David N. Jansen, Minimal Separating Sequences for All Pairs of States, Language and Automata Theory and Applications (LATA 2016), Prague, Czech Republic. March 14–18, 2016.
Abstract:
A way to test software is by Formal State Machine (FSM) testing, and there are several ways to build a test suite. A test suite mostly consists of inputs. These inputs are sequences that distinguish the states in the FSM. We can build these sequences by using a splitting tree or by building an ordered characterizing set.
We first will discuss the method of building a distinguishing set by a splitting tree. A splitting tree partitions the states with a label, which is the sequence that splits the two subsets. The notion of a minimal splitting tree will also be given, and we will show how to build a tree where the separating sequences are of minimal length.
Then we will discuss building an ordered characterisation set (O-Wset), and a bounded version (BO-Wset), which will use notions of a state identification path with a bounded number of transfers or without any transfers. Finding an O-Wset or a BO-Wset is not always possible, and the complexity of this problem is in the NP-complete class. Finally, we will discuss the X3C problem, where we have to find a suitable subset of subsets of all elements, which is a NP-complete problem. This is in order to discuss the mapping of O-Wset to X3C in order to show that it is NP-complete.
Title: Graph Algebras and Partial Combinatory Algebras
Advisor: Sebastiaan Terwijn
Chair: Hilde Ottens
E. Engeler, Algebras and combinators, Algebra Universalis 13, 389-392. 1981.
E. Engeler, Completing the proof of the lemma, unpublished note. June 26, 2021.
Abstract:
Combinatory Algebras are algebraic structures - sets with some operation - that are combinatorially complete, which allows them to act as models of computation. There are two ways to create a completion for a partial combinatory algebra (PCA), weak and strong. In general, PCA's do not have strong completions.
I will explain what Graph Algebras are and how represent any algebra as a Graph Algebra. We will then generalize this operation to algebras with arbitrarily many operations of arbitrary arity, and to partial operations. We will use this graph algebra to create a weak completion for any PCA.
[link to the old page with descriptions of the projects by the teachers]