Anton Golov
A1: Sander Suverkropp
First Steps in Synthetic Computability Theory
Andrej Bauer
MFPS 2006
Computability theory is usually built up by fixing some model of computation
(e.g. Turing machines, partial computable functions) and then saying that
functions are computable if they can be encoded in this model. In this way,
the computability structure becomes something layered on top of our usual
notion of sets and functions. In this paper, Bauer proposes an alternative
approach, whereby we instead change the underlying logic we are working in to
give all sets and functions some computability structure, giving us a more
natural way to introduce notions like decidable and computably enumerable
sets. The paper lays out the axioms of this new logic and uses it to prove
some basic results from computability theory. This material is linked to
category and topos theory on the one hand, being essentially a way of working
internally to the effective topos, and to formalisation on the other, since
this approach is well-suited to being used in a proof assistant like Coq, as
well as having connections to constructive mathematics and topology.
Bas Terwijn
B1: Marten Straatsma
Representing "undefined" in lambda calculus
H. Barendregt
Journal of Functional Programming 2(3), 367-374, 1992
Numerations, lambda-calculus, and arithmetic
A. Visser,
In: J. P. Seldin and J. R. Hindley (eds.), To H. B. Curry:
Essays on Combinatory Logic, Lambda Calculus and Formalism,
Academic Press, 259-284, 1980
Representing partial computable functions in lambda calculus
A p.c. function psi is represented by a lambda term F if
psi(n)=m iff F(#n) = #m
Here #n denotes a term representing the number n, and the =
on the RHS is beta equivalence. The question is what do with
undefined computations. Note that in the lambda calculus all
applications are always defined.
Let A be a set of terms. Say that psi is represented w.r.t. A
if F(#n) is in A whenever psi(n) is undefined. So the terms in A
represent "undefined".
To represent all p.c. functions, several choices for A are
possible. Church used terms without normal form, and Barendregt
the unsolvable terms. The abstract properties of A required for
this were isolated by Statman: It suffices if the complement
of A is a so-called Visser set.
The proof of Statman's theorem uses the ADN theorem of Visser,
which in turn relies on Kleene's recursion theorem.
Goal of this project is to understand this result and the
surrounding material.
Cynthia Kop
C1: Astrid van der Jagt
Proving non-looping non-termination automatically
Fabian Emmes, Tim Enger, Jürgen Giesl
IJCAR 2012
In term rewriting, the question of termination addresses
whether or not there is an infinite reduction sequence.
This paper introduces a technique to prove non-termination;
that is, the existence of such a sequence.
In particular, it seeks to prove non-termination of systems where there
is no infinite loop, but non-termination is
caused by the appearance of a different kind of pattern.
C2: Alex van der Hulst
SAT Solving for Termination Analysis with Polynomial Interpretations
Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René
Thiemann, Harald Zankl
SAT 2007
In term rewriting, the question of termination addresses
whether or not there is an infinite reduction sequence.
This paper discusses how to implement a particular technique to prove
termination; that is, the absence of such a sequence.
In particular, it discusses polynomial interpretations,
essentially a way to give a measure to a term that decreases in each
reduction step, and how to automate the search for suitable
interpretations using modern SAT solvers.
Dario Stein
D1: Tjitske Koster
Objects of categories as complex numbers
Marcelo Fiore, Tom Leinster
Advances in Mathematics Vol 190, 2005
Consider the datatype of binary trees, e.g. written in Haskell as
data T = Leaf | Branch T T
It has been observed by Lawvere and Blass [1] that there exists an explicit
bijection between seven-tuples of such trees and single trees (T^7 ≅ T)! This
bijection can simply be obtained by applying the defining isomorphism of
trees, T ≅ T^2 + 1, repeatedly. If we pretend that T was a complex number, the
solutions of the equation T = T^2 + 1 satisfy T^6 = 1. This is clearly
nonsense in terms of trees, however T^7 = T is indeed another, valid
consequence. The authors study a systematic procedure for when equations over
complex numbers have valid generalizations to more general objects like trees.
Contrary to the title, this paper uses category theory only in superficial
ways. Instead, the methods center around abstract algebra (rings, semirings,
semigroups). For students with more advanced interest in category theory,
Blass' paper [1] is relevant.
[1] Andreas Blass, "Seven Trees in One", Journal of Pure and Applied Algebra
103 (1995) 1-21
Freek Wiedijk
F1: Niek Terol
An Abstract Stack Based Approach to Verified Compositional
Compilation to Machine Code
Yuting Wang, Pierre Wilke, Zhong Shao
POPL 2019
This paper describes a version of the CompCert compiler
called CompCertX.
CompCert is a C compiler by Xavier Leroy and others,
implemented in the functional programming language of the
Coq system, with the correctness of that compiler proved
in Coq as well. CompCert targets an assembly language in
which the runtime stack is only implicit and unbounded:
in the CompCert semantics stack overflow does not exist.
CompCertX improves on CompCert in various ways. It has
an explicit finite stack, it has a flat memory space,
and it has a version of separate compilation called
contextual compilation.
F2: (not assigned)
Formalization Techniques for Asymptotic Reasoning in
Classical Analysis
Reynald Affeldt, Cyril Cohen, Damien Rouhling
Journal of Formalized Reasoning 11(1), 43-76, 2018
This paper describes how to do asymptotic reasoning in Coq.
The paper first describes how this can be implemented using
filters, and then builts a formal version of little-o and
big-O notation on top of this. This is part of an analysis
library on top of the mathematical components library.
The paper also discusses how in a constructive system
like Coq one can formalize classical analysis by adding
a few classical axioms.
Herman Geuvers
H1: Jelmer Firet
Impredicative Encodings of (Higher) Inductive Types
Steve Awodey, Jonas Frey, Sam Speight
LICS 2018
It is well-known that inductive data types can be encoded in
polymorphic type theory, like system F (and also in the type theory of
Coq). These do not completely satisfy all the equalities that one
would want to have, especially the so called "eta-equalities". The
paper improves on this by defining a refinement of the usual
impredicative encoding. The paper uses ideas from HoTT (homotopy type
theory) and also extends the impredicate encoding to so called "higher
inductive types" where equalities can be added as a kind of primitive,
like the normal constructors of an inductive data type.
H2: (not assigned)
The Naturality of Natural Deduction (II): On Atomic
Polymorphism and Generalized Propositional Connectives
Paolo Pistone, Luca Tranchini, Mattia Petrolo
Studia Logica 110, 545-592, 2022
It is well-known that the propositional connectives can all be defined
using an impredicative encoding in polymorphic lambda calculus, system
F. This translation, know as the Russell-Prawitz encoding, is sound,
in the sense that the intuitionistic derivation rules hold for this
encoding. The translation does not preserve the equalities that one
expects for proofs (or proof terms in case one views these systems as
typed lambda calculi, using the Curry-Howard formulas as types
correspondence). The paper studies this problem and various
refinements of the translation to preserve equality on proof terms.
H3: Thomas Somers
Linear lambda-calculus is linear
Alejandro Díaz-Caro, Gilles Dowek
FSCD 2022
Linear logic is a "resource aware" logic, where assumptions are used
exactly once and the multiple use of an assumption is explicitly
recorded. In lambda calculus terminology, a lambda-term is linear if
every bound variable is used exactly once. The paper relates this to
the well-known notion of linearity in algebra. The authors prove a
linearity theorem for an extension of linear logic with addition and
multiplication by a scalar: the proofs of propositions in this logic
are linear in the algebraic sense. This work is part of a wider
research program that aims at defining a logic whose proof language is
a quantum programming language.
Ike Mulder + Robbert Krebbers
I1: Aron van Hof
Relational Compilation for Performance-Critical Applications
Clément Pit-Claudel, Jade Philipoom, Dustin Jamner,
Andres Erbsen, Adam Chlipala
PLDI 2022
The goal of this paper is to build provably-correct programs, that are also
fast.
There are a couple of ways of approaching this problem:
- Write high-level (functional) code. This is easier to prove correct, but it
is difficult to compile this down to efficient machine code. Good compilers
will retain the correctness of your code, but often makes it (much) less
efficient.
- Write low-level code. It is easier to get efficient code, but this is much
harder to prove correct — this requires explicit reasoning about the memory
management.
The paper presents an alternative approach, trying to get the best of both
worlds. The authors provide a tool called Rupicola, inside the Coq proof
assistant. One first writes functional code, and proves it correct in Coq.
Then, one can give Rupicola suggestions on how to efficiently compile such
code down to low-level instructions.
Rupicola is not a traditional compiler: by default, it cannot compile all
valid input programs. Instead, Rupicola "compiles" by doing proof search. For
every high-level input instruction, it looks for a "proof", that is, a
low-level output instruction that has the same behaviour as the input. I think
this is quite a nice idea, and I would like to understand it better.
Jules Jacobs + Robbert Krebbers
J1: Christoph Hoffmeyer
Beyond Relooper: recursive translation of unstructured
control flow to structured control flow (functional pearl)
Norman Ramsey
ICFP 2022
Programming languages have structured control flow constructs such as if,
while, break, continue,
but compilers usually represent all these using unstructured gotos in the
form of control flow graphs.
This paper is about the inverse: converting a control flow graph back to
if, while, break, continue.
If it is not allowed to introduce auxiliary variables, this is not always
possible: a control flow graph can be converted to structured control flow
if and only if its edges can be labeled with F (forward) or B (backward),
such that:
1. The F edges form a DAG (directed acyclic graph).
2. For each B edge x -> y, control flow can only reach x by first visiting
y.
The Beyond Relooper paper claims to have an easy to understand algorithm
that performs the conversion or determines that one must introduce
auxiliary variables.
The algorithm of the paper will be used in a future version of the Glasgow
Haskell Compiler to compile Haskell to JavaScript/WebAssembly, which only
have structured control flow.
The goal is not just to understand and explain this particular algorithm,
but also the difference in expressiveness of while/break/continue versus
goto, and concepts such as (ir)reducibility and dominator trees.
J2: Simcha van Collem
A New Look at Generalized Rewriting in Type Theory
Matthieu Sozeau
JFR 2009
When proving a theorem in a proof assistant such as Coq, we often reason by
substituting equals for equals.
In particular, if we have to prove P(x) and we have H : x=y, then we change
our goal to P(y) using the tactic rewrite H.
Generalized rewriting is a facility that extends this type of reasoning
from equality (=) to other relations such as logical equivalence (P <-> Q),
congruence modulo k (a = b mod k), and even asymmetric relations such
logical implication (->) and less-than-or-equal (<=). In each case we have
a goal P(x) and a hypothesis H : R x y, and if P has the right shape we can
go to P(y) using the tactic setoid_rewrite H.
This paper explains the theory behind generalized rewriting, and how
setoid_rewrite works and how type classes are used to make it extensible.
Robbert Krebbers
K1: David Läwen
Later credits: Resourceful Reasoning for the Later Modality
Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung,
Robbert Krebbers, Lars Birkedal, Derek Dreyer
ICFP 2022
Marnix Suilen + Nils Jansen
M1: (not assigned)
Quantum Partially Observable Markov Decision Processes
Jennifer Barry, Daniel T. Barry, Scott Aaronson
Physical Review A 2014
Partially observable Markov decision processes (POMDPs)
are the standard model for decision-making under
uncertainty. The decision maker (agent) is faced with
uncertainty about the outcomes of their decisions, and
also only has partial knowledge of the system, making the
problem of finding an optimal decision-making strategy
especially hard. Indeed, most problems for POMDPs are
undecidable, and the ones that are decidable range from
PSPACE-complete to EXPTIME-complete.
POMDPs can be extended even further, and one such
extension are quantum partially observable Markov decision
processes (QOMDPs). These models form the quantum analog
of POMDPs. This paper introduces QOMDPs by expressing
the actions and observations via superoperators, and the
states by a Hilbert space. Standard POMDPs are included
in this definition by trivializing the quantum part. Then
they show complexity and computability results for QOMDPs,
and in particular show that a problem that is decidable
for POMDPs is undecidable for QOMDPs, making it a non-empty
generalization.
M2: Gerbrich Kroon
Tropical Geometry of Deep Neural Networks
Liwen Zhang, Gregory Naitzat, Lek-Heng Lim
ICML 2018
Neural networks have shown great success in solving complex
problems. Yet, the theoretical understanding of why they
are so successful is limited. This paper uses tropical
geometry, an area in algebraic geometry that is relatively
unknown outside of pure mathematics, to give precise
descriptions of the workings of deep neural networks.
Tropical geometry studies the geometric properties of
polynomials where multiplication is replaced by (standard)
addition, and addition is replaced by the minimization
of the arguments. A deep neural network can be seen as
a function that maps a vector of real numbers to another
vector of real numbers, possibly of different size.
This paper shows a direct connection between tropical
geometry and functions represented by (feedforward)
neural networks.
Nils Jansen + Marnix Suilen
N1: Daniël van Leijenhorst
Computing Behavioral Distances, Compositionally
Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare
MFCS 2013
Bisimulation metrics extend the standard notion of
bisimulation (exact behavioral equivalence) to a
behavioral distance, stating that two states/systems
are equivalent whenever they behave approximately
the same. This is a particularly useful extension in
the context of probabilistic systems such as Markov
decision processes (MDPs), where the behavior of a system
depends on probabilities that are typically estimated
from data. Computing such distances may be unnecessarily
computationally expensive as the compositional structure
of MDPs can be exploited. This paper discusses how to do
this in such a way that the behavioral distances between
(sub)systems can be composed.
Jurriaan Rot
R1: Finn van der Velde
Completeness Theorems for Kleene Algebra with Top
Damien Pous, Jana Wagemaker
CONCUR 2022
Kleene algebra is a complete axiomatisation of language
equivalence of regular expressions. One of its appealing
aspects is that it is also complete w.r.t. relational
models, giving a fascinating connection between relation
algebra and automata theory. In the paper, the authors
add a "top" constant T to the expressions. In the
model of regular languages, the symbol T has a natural
interpretation as the full language, and it's easy to
axiomatise, with the single equation e <= T. However, in
the relational model, the situation is much more difficult:
the axiom e <= T not enough if we want T to be the total
relation. In the paper it is shown that it suffices to
add the equation e <= e T e to get completeness for the
relational case. The proof goes via graph homomorphisms,
and is really elegant. In fact, on Thursday afternoon
(right after the MFoCS seminar class) it was announced
that this paper won a best paper award at CONCUR!
The project consists in understanding this proof and the
background on Kleene algebra. Subsequently there are
plenty of directions to expand (with a second paper),
in relation algebra and/or Kleene algebra.
R2: Kirsten Hagenaars
Weighted Automata Extraction from Recurrent Neural Networks
via Regression on State Spaces
Takamasa Okudono, Masaki Waga, Taro Sekiyama, Ichiro Hasuo
AAAI 2020
Weighted automata are a quantitative extension of classical
automata. Instead of recognising a language, a weighted
automaton recognises a "weighted language", which assigns
to every word a real number. Their theory is of interest
on its own, but in this project we focus on potential
application: as an abstraction of recurrent neural networks
(RNNs). RNNs are neural networks with state, which take
sequences as input - similarly to weighted automata.
In the paper, it is shown how to extract a weighted
automaton from an RNN. The idea is that this is an
abstraction of the RNN which still nicely represents
(part of) its behaviour, but is much simpler. To do so,
the authors use techniques from automata learning, a family
of techniques for constructing automata by systematically
testing and making observations.
There are plenty of directions to choose from for a second
paper. The paper fits in a line of work on state machine
extraction from neural networks, so this is a natural
direction to explore further. Another natural next step is
to gain a deeper understanding of the learning algorithms
(weighted or not) that are used in the current paper.
Deivid Vale + Cynthia Kop
V1: (not assigned)
A Quantitative Understanding of Pattern Matching
Sandra Alves, Delia Kesner, Daniel Ventura
TYPES 2019
This paper presents a quantitative type system, i.e.,
type systems for which types come along with some numeric measure.
These measures usually hold cost or size information of evaluating
well-typed expressions.
Extending types with this extra information allows us to lift complexity
analysis of programs
(well-typed expressions) to the type system in such a way that properties
such as
typability guarantee not only normalization but also
establish resource bounds to the evaluation of expressions.
Following this program,
the paper proceeds on defining a resource-aware non-idempotent intersection
type systems
for a lambda-calculus equipped with pairing for syntax constructions
representing patterns and terms.
The type systems defined here are used to extract exact bounds on the
complexity of evaluating those patterns.
The main task is understanding these type systems and expanding the proofs
given in the paper.
After studying this paper, the student will have a fairly good image of the
techniques that are
usually used in the subject.
A natural next step is to consider more expressive systems that can
guarantee better execution bounds and/or
capture more complex expressions (programs).
Wieb Bosma
W1: Pavel Zwerschke
Decidability of string graphs
Marcus Schaefer, Daniel Stefankovic
STOC 2001, and
Journal of Computer System Sciences 68, 319-334, 2004
String graphs correspond to representability of logical
relations by intersections of regions in the plane (and
generalize the notions of interval graphs and circular
arc graphs). In this paper it was proven for the first time
that there exists an algorithm to verify that a given
drawing by intersecting strings (the regions can just be
replaced by finite strings) does represent a given finite
graph. The difficulty that had to be overcome was that
earlier it had been shown that such representation may
require an exponential number of intersections. One
main results matches this with an upper bound on that
number, making the problem finite.
Included is a small, nice, proof that not every graph is
representable as a string graph.
After this, the second half of the paper goes in a more
topological direction; alternatively, one could study
the result in one of at least two other papers were the
result is strengthened (despite the potentially large
number of intersections to be inspected) that the
verification can be done in polynomial time (in fact,
that the problem is NP-complete).