Jana Wagemaker
A1: (not assigned)
A Cut-Free Cyclic Proof System for Kleene Algebra
Anupam Das and Damien Pous
TABLEAUX 2017
https://doi.org/10.1007/978-3-319-66902-1_16
https://hal.science/hal-01558132v1/document
In this paper the authors investigate a cyclic proof
system for Kleene algebra (KA). Kleene algebra is the
algebra of regular expressions. The axioms of KA are
sound and complete w.r.t. regular language equivalence:
two regular expressions are provably equivalent using
the axioms if and only if they denote the same regular
language. A cyclic proof system is a proof system where a
proof tree can have cycles. There are certain structural
conditions placed on the proof tree to ensure soundness
of the proof system. In this paper, the authors present
a cyclic proof system for KA and show that it is sound
and complete w.r.t. regular language equivalence. The
end of the paper focuses on complexity of proof search
and validation of proofs. This results in an alternative
proof of decidability being PSPACE.
In this project the first goal is to understand soundness
of the cyclic proof system. A choice can be made what to
focus on afterwards (completeness, or the algorithmic
properties). A second paper can be found in the area
of Kleene algebra or cyclic proofs, depending on what
interests you.
Bálint Kocsis
B1: Sonia Welinder
Theorems for Free!
Philip Wadler
FPCA 1989
https://doi.org/10.1145/99370.99404
The paper presents a method to automatically derive
theorems about polymorphic functions in the formal
system variously known as polymorphic lambda calculus,
second-order lambda calculus, or System F, on which
the type system of the programming language Haskell is
based. The method is a consequence of parametricity, an
important metatheoretic property of this formal system,
which expresses that polymorphic functions behave the
same way at different type instantiations.
As part of this project, the potential student would be
introduced to the area of denotational semantics, that
is, the study of mathematical models of formal systems
(such as programming languages). Furthermore, they would
encounter an application of logical relations, an idea
that underlies many proofs about metatheoretic properties
of typed programming languages. There are several options
for the second paper. For instance, one could study models
of the polymorphic lambda calculus (or the lack thereof)
in more detail, or look at other properties of System F,
such as normalisation. A third option is to consider other
formal systems with similar parametricity properties,
such as systems with ML-style polymorphism or Martin-Löf
type theory.
Cynthia Kop
C1: (not assigned)
A Dependency Pair Framework for Innermost Complexity
Analysis of Term Rewrite Systems
Lars Noschinski, Fabian Emmes, and Jürgen Giesl
CADE 2011
https://doi.org/10.1007/978-3-642-22438-6_32
http://137.226.34.227/Publications/AIB/2011/2011-03.pdf
Term rewriting is a formal system based on oriented equations,
which can be used to express algorithms. Due to their simple, formal
definition, term rewriting systems are well-suited to formal analysis, and
many questions have been studied over the years, such as confluence (if a term
is reduced in two different ways, do you still end up with the same result?),
termination (can evaluation go on forever, or does it eventually stop no
matter what we do?) and complexity (if evaluation eventually stops, how long
does that take?). The topic of this paper is the complexity property. More
precisely, the question of how fast a TRS computes a result is formulated as
runtime complexity: given a start term of a given size n, how many steps can
be taken (as a function of n), to reduce this term to a normal form?
Experience has shown that methods for termination can often be adapted to
show complexity as well -- and this paper is no exception. The dependency pair
approach, a commonly used method for termination analysis, is adapted
here to prove complexity. The great benefit of dependency pairs is that they
allow for a very modular analysis, where large systems can be analysed by
cutting them up into smaller chunks that can each be analysed using different
techniques. This paper considers both the core dependency pair framework for
complexity, and some of the "processors": techniques to simplify part of the
problem into hopefully smaller parts.
Note: prior knowledge of the dependency pair framework for termination is not
necessary. Prior knowledge of term rewriting systems is helpful, but also not
required.
slides
Eline Bovy
E1: (not assigned)
Multi-Model Markov Decision Processes
Lauren N. Steimle, David L. Kaufman, and Brian T. Denton
IISE Transactions, May 2021
https://doi.org/10.1080/24725854.2021.1895454
Markov decision processes (MDPs) are models for sequential
decision-making problems in a stochastic environment,
where choices have probabilistic outcomes. The goal of
the MDP is to find the optimal choices (policies) with
respect to an objective, such as maximizing a reward
or reaching a specific state. To compute these optimal
choices, MDPs require the exact probabilities with which
choices reach certain outcomes. In practice, however,
these probabilities are not always available.
This paper considers Multi-model MDPs (MMDPs) where,
instead of the exact probabilities, we know a set of
possible probabilities. Alternatively, this can be seen
as a set of possible MDPs. The goal this paper looks
at is to compute an optimal policy with respect to a
reward function given a distribution over the possible
models in the MMDP. The paper discusses the complexity,
the optimality of different types of policies, and exact
and approximate algorithms for computing optimal policies.
For a second paper on this subject, one could investigate
complexity or policy optimality results for MMDPs
with other objectives, consider different algorithmic
approaches, or look at related model types, such as MMDPs
with imperfect information.
slides
Herman Geuvers
H1: (not assigned)
What Does It Take to Certify a Conversion Checker?
Meven Lennon-Bertrand
FSCD 2025
https://doi.org/10.4230/LIPIcs.FSCD.2025.27
To certify a proof assistant like Rocq, one want to formalize the
system in Rocq itself and prove that the kernel (the part of Rocq that
forms the trust base of the system) correctly implements the type
theory. The kernel of Rocq is the type checker, so one wants to prove
that the type checking algorithm is
* sound (if the algorithm answers positively on input "G |- M:A", then
G |-M:A holds) and
* complete (if G |-M:A holds then the algorithm answers positively
on input "G |- M:A").
Apart from that one needs to prove that the algorithm terminates on
all inputs which is fundamentally impossible inside Rocq, as it
implies consistency of Rocq (and if Rocq is consistent we can't prove
its consistency in Rocq itself -- see Goedel).
The paper analyzes this situation: to what extent can one formalize
Rocq inside Rocq? It discusses the formalization of Rocq in Rocq (so
it is based on a large formalization) and it focuses in particular on
conversion checking, which is a key ingredient of the type checking
algorithm.
H2: (not assigned)
A Variation of Reynolds-Hurkens Paradox.
Thierry Coquand
LNCS 14560, 2024
https://doi.org/10.1007/978-3-031-61716-4_7
If one extends higher order predicate logic with polymorphic domains,
where "Prop", the domain of propositions, is a basic domain, the logic
becomes inconsistent. This is known as "Girard's paradox" from the
1970s. The problem is usually stated in type theoretical terms, saying
that lambda-U is inconsistent. The non-trivial proof has been studied
and analyzed by Coquand and others in the 1980s and 1990s and Hurkens
made a serious simplification in 1995. This gives a short proof, but the
intuition is hard to grasp. Also the reduction of the proof-term has
been analysed. Coquand has recently given a new presentation, relating
the paradox to Reynolds paradox which states that a set-theoretic
model of polymorphism doesn't exist.
The paper by Coquand is short, but one may need other papers for background.
Jurriaan Rot
J1: Maartje Kramer
Determinisation and Unambiguisation of Polynomially-
Ambiguous Rational Weighted Automata
Ismaël Jecker, Filip Mazowiecki, David Purser
LICS 2024
https://doi.org/10.48550/arXiv.2310.02204
Weighted automata are a generalisation of classical
(non-deterministic) automata, which assign to every word
a weight. In a simple and common form this weight is a
rational number; in the general case weighted automata
can be studied over arbitrary semirings. Contrary to
standard non-deterministic automata, weighted automata
do not determinise in general, in the sense that there
are languages that are recognised by a non-deterministic
but not by a deterministic weighted automaton. In the
paper, the authors study the question whether, for a
given weighted automaton, there exists an equivalent
deterministic automaton (and also whether there exist
an equivalent unambiguous automaton, a relaxation of
determinism). The project would be first to understand
the basics of weighted automata, and then the results
from this paper, or a part thereof.
Loes Kruger
K1: Kati Overbeeke
Efficient state identification for finite state
machine-based testing.
Uraz Cengiz Turker, Robert M. Hierons, Mohammad Reza
Mousavi, and Khaled El-Fakih
IEEE Transactions on Software Engineering, August 2025
https://doi.org/10.1109/TSE.2025.3604472
Finite State Machines (FSMs) are formal models used to
depict the behaviour of a software system and can be used
to guide its testing.
In FSM-based testing, the tester derives a test suite from
the FSM model representing the system's specification.
Often, a test suite generation technique requires
input sequences to check whether the FSM is in the
intended state; this set of input sequences is called a
characterising set.
Even though the use of characterising sets simplifies
testing, they require costly resets and additional
transfer sequences.
This work introduces a class of characterising sets
(Ordered Characterising Sets (O-WSets)) that avoid using
resets or transfers by design.
We show that checking the existence of such a
characterising set is NP-complete.
We introduce the notion of bounded O-WSets (BO-WSets),
which are types of O-WSets that limit transfer usage,
and give an algorithm that constructs these.
Several experiments show reductions in the number of
resets when using the proposed approach.
Lukas Mulder
L1: Codrin Iftode
A Completeness Theorem for Probabilistic Regular
Expressions
Wojciech Różowski, Alexandra Silva
LICS 2024
https://doi.org/10.48550/arXiv.2310.08779
Regular expressions are a mathematical way to capture
computer programs. It supports operations such as
sequential composition ( · ), non-deterministic choice
( + ) and looping by repeating an action zero or more times
( * ). Regular expressions can be compared by computing
their regular language, which consists of all possible
outcomes of the execution of the corresponding computer
program. Comparing regular languages can be done using
transition systems (also called finite state machines
or automata).
In the paper, a probabilistic variant of regular
expressions is proposed where choice is made according
to a probability p ( +p ), and looping repeats zero or
more times probabilistically ( [p] ). Analogous to the
non-probabilistic case, the authors develop probabilistic
regular languages and the corresponding transition systems
and show these can be used to compare probabilistic
regular expressions.
The goal of the project would be to understand the new
concepts proposed and give an overview of the proof of
the main result of the paper. There are many avenues for
a second paper as well.
slides
Márk Széles
M1: Johannes Kool
How long, O Bayesian network, will I sample thee?
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen,
Christoph Matheja
ESOP 2018
https://doi.org/10.1007/978-3-319-89884-1_7
Bayesian networks are a probabilistic graphical model
suitable for expressing conditional dependencies between
random variables. Given such a Bayesian network, one
often wants to infer certain conditional probabilities
that involve the random variables in the network. For
example: `What is the probability of a burglary given
that the alarm went off?' Computing an exact answer to
such queries can be costly, hence one often resorts to
approximate inference techniques. One such technique is
called rejection sampling. This involves drawing samples
from the joint distribution of the Bayesian network,
and keeping only the ones that satisfy the observation
(`the alarm went off'). The samples are then assembled
to an empirical distribution, in which inference can
easily be performed. However, the efficiency of this
method ultimately depends on the expected computation
time required to get a valid sample.
The paper provides a method to compute the expected time
that it takes to get a sample from a Bayesian network
that satisfies a given observation. For this, the authors
transform the Bayesian network into a probabilistic
program, then apply a calculus of expected runtimes
(similar to weakest precondition calculi) to get an
answer. The project would start with studying some basics
of probabilistic programming and Bayesian networks. A
fundamental level of understanding is enough to follow
the paper. For the second paper, there are several
options. These include papers on verification of more
complex probabilistic programs/properties, or papers
about various inference techniques for Bayesian networks.
slides
Niels van der Weide
N1: Erin Leachman
On Krivine's realizability interpretation of classical
second-order arithmetic
Paulo Oliva and Thomas Streicher
Fundamenta Informaticae, January 2008
[no working doi?]
https://www.eecs.qmul.ac.uk/~pbo/papers/paper016.pdf
Realizability is a technique in logic, which is used to
provide interpretations of type theory, set theory, and
Heyting arithmetic. One way to view realizability, is as a
way to make the Brouwer-Heyting-Kolmogorov interpretation
of intuitionistic logic precise. Concretely, one starts
with a partial combinatory algebra (which, intuitively,
represents a notion of computation) from which one creates
a realizability interpretation. While realizability is
usually applied in the context of intuitionstic logic,
extensions to classical logic have been developed. This
paper studies Krivine's realizability interpretation of
classical second-order arithmetic. It shows that Krivine's
realizability interpretation can be seen as a process
of two simpler and well-known steps, namely the double
negation translation and intuitionistic realizability.
slides
N2: Ties Steijn
Evidenced frames: A unifying framework broadening
realizability models
Liron Cohen Étienne Miquey, Ross Tate
LICS 2021
https://doi.org/10.1109/LICS52264.2021.9470514
https://inria.hal.science/hal-03422961/
Realizability is a technique in logic, which is used
to provide interpretations of type theory, set theory,
and Heyting arithmetic. One way to view realizability,
is as a way to make the Brouwer-Heyting-Kolmogorov
interpretation of intuitionistic logic precise. Concretely,
one starts with a partial combinatory algebra (which,
intuitively, represents a notion of computation) from
which one creates a realizability interpretation. However,
there is a slight discrepancy between modern programming
languages and partial combinatory algebras: whereas the
former incorporates various kinds of effects, such as
non-determinism, partiality and states, the latter only
incorporates partiality. This paper provides a way to
extend realizability interpretations to cover computational
effects, which gives us a broader variety of models of
intuitionistic logic. To do so, they introduce the notion
of "Evidenced Frame", which provides a good setting
for broadening realizability models.
slides
Robbert Krebbers
R1: Ard van der Putten
Tree Borrows
Neven Villani, Johannes Hostert, Derek Dreyer and Ralf Jung
PLDI 2025
https://doi.org/10.1145/3735592
The Rust type system gives strong guarantees about programs---not only to
ensure their safety, but it also provides information about whether pointers
are aliased or not, allowing compilers to perform sophisticated optimizations.
This paper is concerned about the correctness of such optimizations,
especially in the presence of `unsafe' code.
The paper defines a semantics for Rust, called "tree borrows". It evaluates
the semantics on 30k of the most widely used Rust crates, formalizes the
semantics in the Rocq proof assistant, and uses the formalization to prove the
correctness of some program optimizations.
For the second paper, you can take a look at the semantics of similar
languages (e.g., C or LLVM), verification of the Rust type system (e.g., the
RustBelt project), compiler verification methods (e.g., CompCert or
SimulIris), or the comparison with other/prior semantics for Rust (e.g.,
Stacked Borrows).
slides
Sebastiaan Terwijn
S1: Thomas Posthuma
Algebras and combinators
E. Engeler
Algebra Universalis, December 1981
https://doi.org/10.1007/BF02483849
https://people.math.ethz.ch/~engeler/g_AlgebrasAndCombinators.pdf
This is a project in combinatory algebra, which is a formalism closely related
to lambda-calculus. However, no particular knowledge about lambda-calculus is
needed. A combinatory algebra is a set with an application operator that
satisfies properties that allow us to view it as an abstract model of
computation. In particular it contains special elements k and s, from which
many familiar functions can be defined. If the application is partial we call
the structure a partial combinatory algebra (pca). It is known that if we
consider k and s as part of the signature then not every pca has a completion.
However, it follows from Engeler [1] that if we allow k and s to vary then
every pca has a completion. The project is to understand the short paper [1],
and it's supplementary note [2], and to compare this result to other kinds
of completions. In particular, the graph algebra from [1] may be compared
to Scott's graph model and to Kleene's second model K_2.
[1] E. Engeler, Algebras and combinators, Algebra Universalis 13 (1981) 389-392.
[2] E. Engeler, Completing the proof of the lemma, unpublished note, June 26, 2021.
Thomas Somers
T1: Ben van Wijngaarden
Interaction Trees:
Representing Recursive and Impure Programs in Coq
Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha,
Benjamin C. Pierce, Steve Zdancewic
POPL 2020
https://doi.org/10.1145/3371119
A key property of compilers is that the compiled program should have the
same behavior as the source program. To formally verify this, it is
necessary to give a semantics to both the source and target programs,
which are then compared. However, operational semantics are not easily
extensible, as effects such as state, input/output, and non-determinism
require explicitly changing the operational semantics and determining
their interactions.
This paper proposes a denotational semantics based on Interaction Trees,
implemented in Rocq (formerly Coq). Inspired by free monads from
functional programming, Interaction Trees are a coinductive variant that
compositionally represents these program effects. To support
non-termination, they include a no-op `tau` operation, where programs
are equivalent when their interaction trees are equivalent modulo `tau`.
The authors develop a compositional library for reasoning about
equivalence and demonstrate its utility by proving correctness of a
compiler from imperative to assembly code.
For the second paper, you could look into the work on algebraic effects
and free monads that inspired interaction trees, applications of
interaction trees for verifying specific programs (program
verification), or alternative program semantics such as operational
semantics.
Simcha van Collem
V1: Floris Reuvers
Propositions as Sessions
Philip Wadler
ICFP 2012
https://doi.org/10.1145/2364527.2364568
The Curry-Howard correspondence makes a connection between logic and type
theory. Propositions are related to types and proofs to programs. This
connection can be extended to a correspondence between a form of linear
logic -- where every assumption has to be used exactly once -- and session types,
which describe communication protocols between concurrent processes while
guaranteeing that messages are sent in the correct order, every send
operation is matched by a receive operation, and deadlock freedom. Propositions
are now related to session types, while proofs are related to processes.
This paper is the first to make this connection formal. It does so by
introducing a processes calculus and a functional language, and presenting a
direct translation from the latter to the former, ensuring communication
safety and deadlock freedom for the functional language.
For a second paper, there are many possible directions. Sessions types have
applications in distributed systems, and their ideas are also adopted by
real-world languages like Rust. Other directions include multiparty session
types (as opposed to the two-way communication considered in this
paper), and exploring language implementation and compiler design.
Wieb Bosma
W1: Hilde Ottens
A Hyper-Catalan Series Solution to Polynomial Equations,
and the Geode
N.J. Wildberger, Dean Rubine
The American Mathematical Monthly, May 2025
https://doi.org/10.1080/00029890.2025.2460966
For linear, quadratic, cubic and quartic polynomials with
rational coefficients it is possible to express zeroes
by a combination of the usual arithmetic operations
combined with root extraction; but it is known since
Abel/Ruffini and Galois that such solutions "in radicals"
are not always possible for degree 5 and higher. In this
paper it is proven that there always exiss a solution
in the form of a particular type of power series, of
which the coefficients have interesting combinatorial
properties --- that is, these "hyper-Catalan" numbers
count certain (geometric) things (essentially numbers of
ways to subdivide n-gons into triangles, quadrilaterals,
pentagons, etc, by drawing non-intersecting diagonals).
There are several nice examples (starting with quadratic
polynomials), and, contrary to the case with the usual
Galois theory for radical solutions, you do not need any
group theory or other advanced algebraic methods.