Title: Proof by linking – transforming proof goals with just two clicks
Advisor: Ike Mulder + Robbert Krebbers
Chair: Rutger Dinnissen
Chaudhuri, K. Subformula Linking for Intuitionistic Logic with Application to Type Theory. In: Platzer, A., Sutcliffe, G. (eds) Automated Deduction – CADE 28. CADE 2021. Lecture Notes in Computer Science(), vol 12699. Springer, Cham. 2021.
Bertot, Y., Kahn, G., Théry, L. Proof by pointing. In: Hagiya, M., Mitchell, J.C. (eds) Theoretical Aspects of Computer Software. TACS 1994. Lecture Notes in Computer Science, vol 789. Springer, Berlin, Heidelberg. 1994.
Abstract:
Proof assistants have a lot of bookkeeping when proving; many commands have to be issued to move formulas around, break things up and put the formulas back together again (elim/intro patterns). This talk will introduce you to a framework in which these patterns are done much more graphically than with the usual commands: clicking on two nodes in a formula to bring them together – to link them – automatically.
Related material that will be presented are a live demo in a tool called ProfInt, a precursor to linking – called "pointing", a variant that only clicks on one node – and various extensions that you could add to these frameworks.
Title: Proving properties of C programs using localization
Advisor: Marc Hermes + Robbert Krebbers
Chair: Cas Haaijman
Reynolds, John C. Separation Logic: A Logic for Shared Mutable Data Structures. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, LICS '02. 2002.
Shengyi Wang, Qinxiang Cao, Anshuman Mohan and Aquinas Hobor. Certifying Graph-Manipulating C Programs Via Localizations Within Data Structures. Proceedings of the ACM on Programming Languages 3, OOPSLA 2019.
Abstract:
Data structures often exhibit graph-like patterns, particularly when implemented using pointers in the heap. Such implementations present unique hurdles for formal verification: they may permit cycles and shared nodes, complicating the establishment of invariants, and their operations often require pointer manipulation which may affect the global structure in complex ways.
We will explore how separation logic in general and the LOCALIZE proof rule in particular can be used to enable modular reasoning, by focusing in on specific heap segments relevant to the program's execution.
Title: Apartness on Domains of Real Number Computation
Advisor: Niels van der Weide
Chair: Sergio Domínguez Cabrera
De Jong, T. P. Apartness, sharp elements, and the Scott topology of domains. arXiv (Cornell University). 2021.
Di Gianantonio, P. Real number Computability and Domain Theory. Information & Computation, 127(1), 11–25. 1996.
Abstract:
When we think of real numbers, we think of potentially infinite streams of digits. As domain theory is naturally suited for modeling such infinite objects, it lends itself as the theoretical backdrop of formalising real number computation. Computing with such, we eventually end up wanting to compare two real numbers.
However, due to their infinite nature, determining equality for two reals would require potentially infinite evidence. Much easier is the opposite notion: if two reals are unequal, finite evidence suffices; we only require to know on which digit they diverge.
Constructively, we can formulate a positive notion of inequality: apartness. By necessity, apartness must be 'weaker' than classical inequality and lacks properties like cotransitivity that we might desire. The main paper of this presentation studies a concrete apartness relation, intrinsic apartness, providing us with so called 'sharp' elements and an especially well-behaved subclass of 'strongly maximal' elements.
For sharp elements, the intrinsic apartness relation 'gains back' the previously lacking properties.
BIBLIOGRAPHY
This presentation mainly focuses on presenting the results of the following paper by T. De Jong, which studies apartness in a constructive, domain theoretic setting. As a secondary paper, P. Di Gianantonio gives a general perspective on domain theoretic real number computation. Supplementary to this, A. Bauer and I. Kavkler's paper on real number computation is more explicitly constructive.
Bauer, A., & Kavkler, I. A constructive theory of continuous domains suitable for implementation. Annals of Pure and Applied Logic, 159(3), 251–267. 2009.
The details of the domain theoretic preliminaries in this presentation were informed by the introductory work of S. Abramsky and A. Jung.
Abramsky, S., & Jung, A. Domain theory. In Oxford University Press eBooks (pp. 1–168). 1995.
Smaller citations of other works not listed here will be credited as such in the presentation.
Title: Completeness of Kleene Algebra
Advisor: Jurriaan Rot
Chair: Jorrit de Boer
Tobias Kappé. Lecture notes. Course on Kleene Algebra, ILLC, University of Amsterdam.
Damien Pous, Jana Wagemaker. Completeness Theorems for Kleene Algebra with Top. LIPIcs, CONCUR 2022.
Abstract:
Kleene algebra is a generalization of regular expressions. It is used to prove equivalency between regular expressions, where two regular expressions are equivalent if they model the same language. For example, the regular expressions (a + b) and (b + a) are equivalent.
One can derive if two regular expressions are equivalent with a set of axioms. This will be presented in the first part of the presentation, as well as its soundness and completeness (i.e. equivalent regular expressions should result in the same language). Aside from the language model, we also introduce the relational model for regular expressions.
For the second part of the presentation, we add the Top symbol to the syntax of regular expressions. It is interpreted as the full language, like (a + b + c + ...)*. Adding Top means that more axioms are needed to keep the axiomatization sound and complete. We also show that the language and relational models are no longer equivalent in Kleene algebra with Top.
Title: Compositional learning of Automata
Advisor: Loes Kruger + Jurriaan Rot
Chair: Sipho Kemkes
Labbaf, F., Groote, J.F., Hojjat, H., Mousavi, M.R. Compositional Learning for Interleaving Parallel Automata. In: FoSSaCS 2023. LNCS, Springer (2023).
Neele, T., Sammartino, M. Compositional Automata Learning of Synchronous Systems. In: Lambers, L., Uchitel, S. (eds.) FASE 2023. Lecture Notes in Computer Science, Springer (2023).
Abstract:
Automata learning can be used to learn models of black-box systems such as communication- or security protocols.
Often, these models are composed out of components that are either completely independent, or independent with
some synchronization. The papers we look at propose algorithms that are more efficient than the original automata-learning algorithm L* in these cases. They propose compositional approaches which try to learn individual
components and then combine the result.
Title: Generalizing monads to arrows
Advisor: Dario Stein
Chair: Adam Kjelstrøm
John Hughes. "Generalising monads to arrows". Science of Computer Programming, Volume 37, Issues 1–3, pp 67-111 (2000).
Mario Román. "String Diagrams for Premonoidal Categories". arXiv preprint arXiv:2305.06075 (2023).
Abstract:
Monads have engrained themselves as a key part of functional programming languages over the course of recent decades. However, as libraries are becoming more and more sophisticated their limitations are starting to show. In this talk we introduce arrows, which are constructs which generalize monads in new and elegant ways. An arrow is an abstract construct which represents impure computations. Arrows can be composed (non-commutatively) with other arrows to create general impute programs. Extensions allow for more complex operations over arrows, such as monoid operations, a choice operator, and recursive computations.
We also discuss string diagrams, which provide a graphical way of viewing programs making use of arrows. String diagrams visually depict the flow of a program, connecting functions with functions and values whenever one uses the other. The key insight is that a runtime wire can be used to enforce non-commutativity, allowing for the introduction of impure operations.
Title: Faster Monads with Kan Extensions
Advisor: Dario Stein
Chair: Willem Lambooij
David Reutter, Jamie Vicary, High-level methods for homotopy construction in associative n-categories. LICS '19: Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, June 62, 1–13. 2019.
Hinze, R. Kan Extensions for Program Optimisation Or Art and Dan Explain an Old Trick. In: Gibbons, J., Nogueira, P. (eds) Mathematics of Program Construction. MPC 2012. Lecture Notes in Computer Science, vol 7342. Springer, Berlin, Heidelberg. 2012.
Abstract:
One of the most common approaches for optimizing monadic computations involves
transforming the monad from direct style to continuation-passing style (CPS), which
(may) yield speedups while preserving the semantics of the original computation.
The theoretical underpinnings of this approach rely on the categorical notion of
Kan extension. Every Kan extension induces a monad (the codensity monad) which
is isomorphic to the original and is the categorical counterpart of the CPS
transformation.
Categories, functors, and natural transformations form a 2-category that lends itself to a 2-dimensional notation known as string diagrams. The notation has been extended to higher categories and is used to reason about higher-dimensional structures. Working with higher-dimensional structures can be back-breaking and error-prone, so we use the proof assistant homotopy.io to verify (some of) our results.
Title: An insight into bidirectional type systems
Advisor: Herman Geuvers
Chair: Menzo van Kessel
Thierry Coquand, An algorithm for type-checking dependent types, Science of Computer Programming, Volume 26, Issues 1–3, Pages 167-177, ISSN 0167-6423. 1996.
Meven Lennon-Bertrand, Complete Bidirectional Typing for the Calculus of Inductive Constructions, 2021.
Abstract:
Unlike unidirectional type systems which only define a single mode of
judgment, bidirectional type systems define type checking and type
inference as separate but co-dependent judgment modes. In this talk I
will introduce the basics of bidirectionality and describe two such
systems, one based on a simple dependent type system with un-annotated
abstractions (church-style), and one that is complete with respect to
the calculus of inductive constructions.
Title: Hardness vs Randomness
Advisor: Bas Terwijn
Chair: Jakob Wuhrer
Noam Nisan and Avi Wigderson. Hardness vs Randomness. J. Comput. Syst. Sci., 49(2):149–167, October 1994.
Russell Impagliazzo and Avi Wigderson. P = BPP if E Requires Exponential Circuits: Derandomizing the XOR Lemma. In Proceedings of the Twenty-ninth Annual ACM Symposium on Theory of Computing, STOC '97, pages 220–229, New York, NY, USA, ACM. 1997.
Abstract:
In their 1997 paper, Impagliazzo and Wigderson showed that P=BPP unless E has sub-exponential circuits. E (= TIME(2^O(n))) having sub-exponential circuits is a very unlikely statement and believed to be false. Which means that it is likely that P=BPP, which would mean that every efficient randomized algorithm can be derandomized into an efficient deterministic algorithm, which is a remarkable result.
In the presentation I will show how the existence a function in E that has no sub-exponential circuit, loosely said the existence of a hard to compute function, implies P=BPP. The proof of this implication reveals that hardness and randomness are very closely related, and that something may look purely random because it is too hard to predict, not because it is actually random.
Title: The Hartmanis-Stearn problem and some weaker results
Advisor: Wieb Bosma
Chair: Dick Blankvoort
Boris Adamczewski, Julien Cassaigne and Marion le Gonidec. "On the computational complexity of algebraic numbers: the Hartmanis-Stearns problem revisited". Transactions of the American Mathematical Society 373(5), 2016.
J. Hartmanis and R.E. Stearns. "On the computational complexity of algorithms". Transactions of the American Mathematical Society, 117, 1965.
Abstract:
In 1965 J. Hartmanis en R.E. Stearns published a paper with a still unsolved problem. This problem is about the computational complexity of irrational algebraic numbers computed by finite multitape Turingmachines. Due to the difficulty of this problem, there are some weaker results that are proven. We will look at one of these results in detail: The base-b expansion of an algebraic irrational number cannot be generated by a deterministic pushdown automaton. We will also see some other results and what all of these means in practice.
Title: An Extensible Method for Polynomial Invariant Generation
Advisor: Kasper Hagens + Cynthia Kop
Chair: Lean Ermantraut
Steven de Oliveira, Saddek Bensalem and Virgile Prevosto. Polynomial invariants by linear algebra. ATVA 2016.
Daneshvar Amrollahi, Ezio Bartocci, George Kenison, Laura Kovács, Marcel Moosbrugger and Miroslav Stankovič. Solving Invariant Generation for Unsolvable Loops. SAS 2022.
Abstract:
A loop invariant is a mathematical expression that is true (1) immediately before executing a loop, and (2) at the end of each step of the loop. Loop invariants yield useful insights into software behaviour, but automatically deriving these is well-known to be undecidable in the general case. In view of this, we examine automated methods that under-approximate the question, meaning reported invariants are indeed invariants, but there may be invariants which go unreported. This presentation initially examines a class of loops known as linear loops to show how invariants of a certain form can be automatically derived in this case. This basic method is then extended to handle (1) constants and (2) polynomial assignments under certain conditions. We furthermore discuss how this method can be extended to handle certain non-deterministic behaviour. Finally, we examine how the conditions required on polynomial assignments can be relaxed to allow finding some invariants in this case.
Title: Solving Zero-Sum One-Sided Partially Observable Stochastic Games (POSGs) using Heuristic Search Value Iteration (HSVI)
Advisor: Eline Bovy + Nils Jansen
Chair: Ioannis Koutsidis
Karel Horák, Branislav Bošanský, Vojtěch Kovařík, Christopher Kiekintveld. Solving zero-sum one-sided partially observable stochastic games. Artificial Intelligence, Volume 316, 2023.
Trey Smith and Reid Simmons. Heuristic search value iteration for POMDPs. In Proceedings of the 20th conference on Uncertainty in artificial intelligence (UAI '04). AUAI Press, Arlington, Virginia, USA, 520–527. 2004.
Abstract:
Many competitive interactions between two parties can be modelled using
POSGs, with security games being a relevant real-world apllication.
Nevertheless, solving such a game exactly quickly becomes computationally
intractable even with simple games, i.e., games with little states and
player actions etc. Herein, the restriction is made to reason over
one-sides games which eliminates the partial observability of player two
who is now assumed to have full information and will thus, because of the
strictly competitive nature (zero-sum), be the toughest opponent possible
. A welcome implication: any strategy for player one obtained from solving
such a one-sided zero-sum POSG can be applied as a *robust* strategy in the
real-life scenario that the game us modelled to.
In the seminar, aside from discussing the problem and the approximative method of solving from a high-level perspective, we delve into to some details that allow us to gain an understanding of how the effective HSVI algorithm can be applied to the context of infinite horizon zero-sum one-sided POSGs. In essence, this defines an extension to HSVI, which was originally developed for Partially Observable Markov Decision Processes (POMDPs). As a cherry on the cake, HSVI results are shown to enable us to obtain ε-Nash equilibrium strategies for both players.
[link to the old page with descriptions of the projects by the teachers]