Bálint Kocsis
B1: Lyra van Bokhoven
A taste of linear logic
Philip Wadler
MFCS 1993
Traditional (intuitionistic) logic is about truth:
propositions can either be true or false. The truth of a
proposition is free: having proved a theorem, we may use
this proof as many times as we wish. Linear logic, on the
other hand, is a "resource-conscious" logic: propositions
are not solely about truth, but they carry a notion of
resource. Consequently, assumptions may not be freely
copied or discarded, but each assumption must be used
exactly once. For instance, if A denotes the proposition
"I have 5 euros" and B denotes the proposition "I have a
cake", then the implication A -> B denotes the proposition
"If I have 5 euros, then I can buy a cake". Note that when
we eliminate this implication, the original assumption
"I have 5 euros" no longer holds.
Via the Curry-Howard correspondence between logic and type
theory, intuitionistic logic with implication, conjunction,
and disjunction corresponds to simply typed lambda calculus
with product and sum types. This correspondence can be
extended to linear logic to obtain linear lambda calculus,
whose type system allows for fine control over resources
in a program. Among other things, this type system can be
used to efficiently work with mutable arrays in a purely
functional language.
As possible further papers on this subject, one could study
the proof theory or semantics of linear logic, investigate
further applications of linear type systems to functional
programming, or study other types of substructural (program)
logics such as the logic of bunched implications.
Cynthia Kop
C1: Pieter-Jan Lavaerts
A Dependency Pair Framework for Innermost Complexity Analysis of Term
Rewrite Systems
Lars Noschinski, Fabian Emmes, Jürgen Giesl
CADE 2011
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 in a modular way. (Note: prior knowledge of the
dependency pair framework for termination is not necessary.) The paper lists
several methods, within one bigger framework, to obtain complexity results.
slides
Dario Stein
D1: Bas van der Linden
Backpropagation in the Simply Typed Lambda-Calculus with Linear Negation
Aloïs Brunel, Damiano Mazza, Michele Pagani
POPL 2020
What is the derivative of a higher-order function like `fold`? Automatic
Differentiation (AD, Backpropagation) is the bread-and-butter algorithm
of optimization and machine learning and forms the basis of frameworks
such as PyTorch and Jax. In its simplest form, it takes a computational
graph of a function and produces a new computational graph which
computes the function along with its derivatives (gradient).
This work is about extending AD from mere computational graphs to an
actual programming language, with constructs such as lists,
lambda-abstraction and higher-order functions. The authors define
automatic differentiation macros which operate compositionally on these
constructs. They prove the macros correct, and explain which role
linearity (in the sense of linear functions, but also linear logic)
plays for the effiency of their AD translation.
D2: Donald Scheuring
Practical Probabilistic Programming with Monads
Adam Ścibior, Zoubin Ghahramani, and Andrew D. Gordon
Haskell 2015
Probabilistic Programming is a fascinating new programming paradigm
where a programming language is enriched with commands `sample`,
`observe` and `infer`. Those allow probabilistic choices to be made, to
be conditioned on observations, and the statistical outcomes of the
observations to be learned. Because of Haskell's powerful effect system
based on monads, Haskell can be made into a probabilistic language as
easily as writing the right monad that supports the three commands.
The authors of this paper discuss such monads, and how different monad
designs are suited to different inference algorithms of varying
efficiency. Your talk could be a general introduction to probabilistic
programming, including other languages or applications (economics,
neuroscience etc), or a deeper exploration of some inference algorithms.
Eline Bovy
E1: Niels van Duijl
Robust Markov Decision Process: Beyond Rectangularity
Vineet Goyal and Julien Grand-Clément
Mathematics of Operations Research 2023
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 with respect to
an objective, such as maximizing a reward or reaching a
specific state. In order to compute these optimal choices,
MDPs require the exact probabilities with which choices reach
certain outcomes. In practice, however, these probabilities
often must be estimated from noisy data.
Robust MDPs alleviate this problem by replacing the exact
probabilities with a set of possible probabilities, called
the uncertainty set. The goal of the robust MDP is to compute
the optimal choices in the worst-case situation, with the
worst-case probabilities from the uncertainty set. Various
algorithms have been developed to compute optimal choices
in robust MDPs, but these require additional assumption on
independence between the probabilities.
Such independence assumptions are not always
appropriate. Take, for example, the health evolution
of a patient, where choices must be made regarding
the treatment. Underlying factors such as a patient's
genetics or demographics influence the chance of success
of many treatments. The probabilistic outcomes between
treatment choices are, therefore, not independent. Assuming
independence here will lead to overly conservative treatment
choices.
This paper considers robust MDPs with a weaker
independence assumption and proves fundamental results
leading to an efficient algorithm to compute the optimal
choices. Additionally, they lift classic results from MDPs
to robust MDPs. Finally, their experiments demonstrate that
this paper's approach can be used as a less conservative
alternative to existing robust MDP approaches.
Freek Wiedijk
F1: Rutger Broekhoff
Lean4Lean: Towards a formalized metatheory for the Lean theorem prover
Mario Carneiro
submitted to ITP 2024
The kernel of the Lean proof assistant, which implements
the logic of Lean (a dependent type theory that is very
similar to the one of Coq), is written in C++. This paper
describes a project to formalize this type theory in Lean,
and also implement the kernel in the functional language
of Lean itself. This makes it possible to develop the
metatheory of Lean formally, and to prove the correctness
of the implementation of this kernel.
Possible things to look at are the details of the type
theory of Lean, the metatheory of Lean, the MetaCoq project
(which is a similar project for Coq), and the Lean code of
the Lean4Lean project.
F2: Erik Oosting
Fast, Verified Computation for Candle
Oskar Abrahamsson, Magnus Myreen
ITP 2023
In proof assistants based on dependent type theory, like Coq
and Lean, computation is part of the logical foundations.
This makes both the rules of the logic complex, as well
causes the trusted code base of the proof assistant to be
large, because this code has to include the implementation
of a functional programming language.
In proof assistants based on higher order logic, like
HOL4 and HOL Light, there is no computation in the logical
foundations, which makes everything very clear and simple.
However, one still would like to extend this logic with rules
for computation. This paper describes an approach for this.
This work is part of the CakeML project. CakeML is a
verified ML compiler, implemented and verified using the
HOL4 proof assistant. There is a verified proof assistant
called Candle developed in this project, which is a port
of the HOL Light proof assistant, where the kernel is
implemented in HOL4 and the rest is implemented in CakeML
(ported from OCaml).
Possible other papers to look at are about the background
of this work in the CakeML/Candle project.
Herman Geuvers
H1: Remco van Os
Minimal Depth Distinguishing Formulas Without Until for Branching Bisimulation
Jan Martens, Jan Friso Groote
LNCS 14560, 2024
Labelled transition systems (LTS) describe processes in terms of
states and labelled transitions between these states. An important
question is when two states should be considered "equal" or dually,
when they should be seen as "different". It is standard to consider
two states equal in case they are _bisimilar_ which is a coinductively
defined notion that captures the idea that two states are equal in
case one can make the same observations on them. Recently, the dual
notion of bisimulation, _apartness_ has also been studied in its own
right: two states are apart in case there is an observation that
distinguishes them. Apartness is an inductive notion and can be
characterized via a deduction system: two states are apart in case we
can make a derivation (using the deduction rules for apartness) of
that fact.
What the precise definition of bisimulation (resp. apartness) is
depends on what one considers "observable". An interesting case occurs
when the LTS has "silent steps", also called tau-steps: steps that a
system can take that are not observable from the outside. Then the
most used notion is "branching bisimulation" (and dually "branching
apartness").
There is also a logical view on states of an LTS provided by
Hennessy-Milner (HM) logic . This is a modal logic with the idea that
a modal formula phi holds in a state s in case phi correctly describes
the possible observations that can arise when process-execution starts
in s. In fact there are variants of HM logic for each notion of
bisimulation such that an HM theorem holds: states s and t are
bisimilar iff for all HM logic formulas phi (phi holds in s iff phi
holds in t). Or, phrasing it in terms of apartness: states s and t are
apart iff there is a HM logic formula phi such that (phi holds in s
and phi does not hold in t). A HM logic formula phi that distinguishes
s and t gives a kind of high level (i.e. in purely logical terms)
explanation of why s and t are different.
The paper studies the question of finding a minimal depth formula that
distinguishes two states, where the depth is measured in terms of the
number of nested modalities. Traditionally, the HM theorem for
branching bisimulation uses so called "HM logic with until", where
"until" is a binary modality. The present paper uses a unary
modality, and it uses the apartness view in its proofs.
slides
H2: (not assigned)
Mechanized Subject Expansion in Uniform Intersection Types for Perpetual Reductions
Andrej Dudenhefner, Daniele Pautasso
FSCD 2024
Also read:
From Normalization to Typability via Subject Expansion
Andrej Dudenhefner
ITRS 2024
For typed lambda calculi, the property of "normalization" for
beta-reduction is a central result, where one can distinguish between
"weak normalization", WN, (for every term M, there is a reduction path
from M that leads to a normal form) and "strong normalization", SN,
(for every term M, every reduction path from M eventually
terminates). For simple type theory there are various proofs of WN and
SN. For interection typed lambda calculi, there is even a stronger
result (*): M is typable iff M is SN. The implication from left to right
is known since the invention of intersection types, while the
implication from right to left has been proved several times, but
often with wrong (incomplete) proofs, as the authors remark (and
several others have remarked that as well).
The present paper studies normalization by defining refined notions of
beta-reduction. It is well-known that we can split up beta-reduction
in I-reduction and K-reduction steps, where I-reduction reduces
(\x.M) N -> M[x:=N] if x in FV(M)
and K-reduction reduces
(\x.M) N -> M if x notin FV(M).
A K-reduction can "throw away" an infinite reduction path, so for the
study of SN, one would like to limit to I-reduction. However, a
K-reduction may sometimes be needed to "unblock" an I-redex and
therefore people have added so-called gamma-reduction steps. The
present paper follows a different track and introduces K'
reduction. As its main results it gives a new proof of the result (*)
above and a new original proof of SN for simple type theory.
slides
Jana Wagemaker
I1: Simon Ruiz
An Elementary Proof of the FMP for Kleene Algebra
Tobias Kappé
RAMiCS 2023
I am linking to the preprint of the journal version.
Kleene algebra (KA) is the algebra of regular expressions
and is a useful tool for proving that two programs are
equivalent. This works well because the theory of KA is
well-developed. In particular, it is shown to be decidable
and complete. In the nineties, KA was shown to be a complete
axiomatisation of equivalence of regular languages. Shortly
after, KA was also proven complete w.r.t relational
models. Then, in 2005, it was shown that the finite model
property (FMP), which states that false equivalences always
have a finite counter example, is equivalent to completeness
over language models for KA. A direct proof of this FMP was
missing. In the paper, this proof is provided. Moreover,
the paper studies the model theory of KA, and explores
connections between relational models of KA and the finite
model property.
The project consists of understanding the proof of the finite
model property, which uses automata techniques not used in
the previous completeness proofs of KA, and the model theory
of KA. A second paper can for instance be chosen in the area
of relational algebras, or (background) on Kleene algebra.
I2: Lukas Nieuweboer
Deciding Hyperproperties
Bernd Finkbeiner, Christopher Hahn
CONCUR 2016
Hyperproperties are a generalisation of trace properties:
a trace property is a set of traces, and a hyperproperty is
a set of sets of traces. They can be applied for instance in
information flow security by characterising properties of a
system that involve two or more execution traces. There are
various logics to specify hyperproperties, and a common one
is HyperLTL, which extends LTL (Linear-time temporal logic)
to hyperproperties. The paper investigates satisfiability
of HyperLTL. They show that for alternation-free formulas
the problem is PSPACE complete, and no more expensive than
LTL satisfiability, for formulas that start with a string
of exists quantifiers followed by for all quantifiers,
the problem is EXPSPACE complete, and undecidable for
formulas that start with a for all quantifier followed by
an exist quantifier.
The project consists of understanding the proofs of the
decidability results, and the background on HyperLTL and
LTL. There are plenty of second papers that can be chosen
in the area of HyperLTL or LTL.
Jurriaan Rot
J1: Daan Spijkers
Algebraic Recognition of Regular Functions
Mikolaj Bojańczyk, Lê Thành Dũng Nguyễn
ICALP 2023
Regular languages have numerous equivalent descriptions -
they can be captured through regular expressions, DFAs,
NFAs, Myhill-Nerode, certain logics, semigroups, and
more. When moving from languages to functions between
words (and languages), the notion of regular is a bit more
subtle; it emerges to be the class captured by streaming
string transducers, again certain logics, 2DFAs, and some
other models. In the current paper, the authors show that
these functions can equivalently be captured by a certain
type of functor (on the category of semigroups) together
with a natural transformation. The aim of this project is
to understand how this categorical presentation captures
regular functions, and the equivalence with existing models
of regular functions, shown in the paper. There are plenty
of opportunities for a second paper; for instance, a more
in-depth study of any of the other equivalent models of
regular functions. The paper uses category theory but
this is not a prerequisite; only very little category
theory is needed, and this can be picked up along the
way. Some familiarity with automata theory is needed (a
basic introductory course on automata theory suffices).
Komi Golov
K1: Tanja Muller
Linearity and Uniqueness: An Entente Cordiale
Daniel Marshall, Michael Vollmer, Dominic Orchard
European Symposium on Programming 2022
Rust has pushed linear types into the mainstream, making them—and
substructural type systems more broadly—a hot topic in PL circles. Linear
types are easily confused with uniqueness types: both have a restriction on
something being exactly once. This paper spells out exactly what the relation
between the two is, and shows how they can be combined in a single programming
language. The crux of the story is that when uniqueness or linearity is
enforced throughout the system, the two coincide; however, when a system
allows weakening one or the other, they diverge. This is shown by comparing
the non-linear modality ! with the non-unique modality °, and then introducing
a linear lambda calculus with a non-linearity and a uniqueness modality.
This project will be about understanding the relation between uniqueness and
linearity, as well as the lambda calculus introduced in the paper. Possible
second papers include follow-up papers by the coauthors, or comparing this to
other work on uniqueness or linearity.
Loes Kruger
L1: Jasper Laumen
Automata Learning with an Incomplete Teacher
Mark Moeller, Thomas Wiener, Alaia Solko-Breslin, Caleb Koch,
Nate Foster, Alexandra Silva
ECOOP 2023
Active automata learning is used to infer a DFA from a
system of which we do not know the internal behavior. These
learning algorithms assume the existence of an idealized
oracle - a so-called Minimally Adequate Teacher (MAT)
- that cannot be fully realized in practice and so is
usually approximated with testing. This paper proposes a
new framework for active learning based on an incomplete
teacher. This new formulation, called iMAT, adapts the L*
algorithm to handle scenarios where the teacher only has
access to a finite set of positive and negative examples
and uses SMT solving to fill in the gaps.
Niels van der Weide
N1: Mark Lapidus
Type Theory with Explicit Universe Polymorphism
Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó
TYPES 2022
Universes are an important feature in type theory, because
one can use them to define polymorphic functions like the
identity function. However, since it is inconsistent to
have a universe containing itself by Girard's paradox,
many flavors of type theory come with a countable chain
of universes. This poses another challenge: now we
have an identity function for each universe. Instead of
these functions separately, we would like to define them
polymorphically. The feature of type theory that allows
us to do this, is known as universe polymorphism. The
paper "Type Theory with Explicit Universe Polymorphism"
discusses a type theory with a countable chain of universes
and explicit universe polymorphism. and briefly discusses
how it compares to universe polymorphism in several proof
assistants like Coq, Agda, and Lean.
slides
N2: Jakub Dreżewski
Constructive set theory
John Myhill
JSL 1975
In the previous century, there have been various developments
of mathematics in constructive foundations. Among those,
is the book "Foundations of constructive analysis" by
Errett Bishop, where a significant part of real analysis
is developed constructively. However, Bishop used natural
language instead of a formal logical system. In the paper
"Constructive Set Theory" a formal system, called CST
(nowadays known as CZF), is given, which is able to codify
the mathematics by Bishop. More specifically, the author
describes a constructive version of Zermelo-Fraenkel
set theory. Finally, the author proves that a restricted
version of this system satisfies the existence property,
which intuitively says that whenever you can prove that a
certain term exists, then you can also construct it.
slides
Robbert Krebbers
R1: Dick Arends
Verified Extraction from Coq to OCaml
Yannick Forster, Matthieu Sozeau, Nicolas Tabareau
PLDI 2024
Extraction is the process of turning programs and proofs in the
dependent type theory of a proof assistant into efficient programs in a
mainstream (functional) language such as Haskell or OCaml. Extraction
plays an essential role in CompCert, a verified optimizing C compiler
written in Coq and extracted to OCaml (https://compcert.org/).
The current implementation of extraction in Coq is not verified, so it
is unclear whether the extracted (target) OCaml program has the same
semantics as the (source) program/proof written in Coq. Also there is no
way to reason about the correctness when linking the extracted code to
manually written OCaml code. This paper addresses both problems through
a new version of extraction implemented and verified in Coq itself.
You should select this project if you like proof assistants, semantics,
functional programming, compilers, and bootstrapping.
Part of this paper is an implementation
https://github.com/yforster/coq-verified-extraction, I strongly
encourage to play with that.
Sebastiaan Terwijn
S1: Lorenzo Bafunno
[1] Algebras and combinators
Erwin Engeler
Algebra Universalis 13, 1981
[2] Completing the proof of the lemma
Erwin Engeler
unpublished note, 2021
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 its 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.
Wieb Bosma
W1: (not assigned)
On Unsettleable Arithmetical Problems
J. H. Conway
The American Mathematical Monthly, 2013
In this paper Conway argues that it is very likely that
a particular variant of the famous Collatz conjecture
(or 3x+1 problem) is "unsettleable" --- that is, is one of
the problems (known to exist since Go"del's
incompleteness results) that we can neither prove
nor disprove.
It is useful to also look at his 1972 paper, or to look
at Fractran (universal computation system), or if you
prefer, look at the connection to Post's tag systems
as in the paper by Liesbeth de Mol, `Tag systems and
Collatz-like functions', Theoretical Computer Science
390 (2008) 92–101.