Anton Golov

A1: (not assigned)

CQS: A Formally-Verified Framework for Fair and Abortable Synchronization Nikita Koval, Dmitry Khalanskiy, Dan Alistarh PLDI 2023 Writing concurrent code that is both correct and efficient is notoriously difficult. Thus, programmers often prefer to use synchronization abstractions, which render code simpler and easier to reason about. Despite a wealth of work on this topic, there is still a gap between the rich semantics provided by synchronization abstractions in modern programming languages—specifically, fair FIFO ordering of synchronization requests and support for abortable operations—and frameworks for implementing it correctly and efficiently. Supporting such semantics is critical given the rising popularity of constructs for asynchronous programming, such as coroutines, which abort frequently and are cheaper to suspend and resume compared to native threads. This paper introduces a new framework called CancellableQueueSynchronizer (CQS), which enables simple yet efficient implementations of a wide range of fair and abortable synchronization primitives: mutexes, semaphores, barriers, count-down latches, and blocking pools. Our main contribution is algorithmic, as implementing both fairness and abortability efficiently at this level of generality is non-trivial. Importantly, all our algorithms, including the CQS framework and the primitives built on top of it, come with formal proofs in the Iris framework for Coq for many of their properties. These proofs are modular, so it is easy to show correctness for new primitives implemented on top of CQS. From a practical perspective, implementation of CQS for native threads on the JVM improves throughput by up to two orders of magnitude over Java's AbstractQueuedSynchronizer, the only practical abstraction offering similar semantics. Further, we successfully integrated CQS as a core component of the popular Kotlin Coroutines library, validating the framework's practical impact and expressiveness in a real-world environment. In sum, CancellableQueueSynchronizer is the first framework to combine expressiveness with formal guarantees and solid practical performance. Our approach should be extensible to other languages and families of synchronization primitives.
Bas Terwijn B1: Jorrit de Boer
P = BPP if E requires exponential circuits: derandomizing the XOR lemma Russell Impagliazzo, Avi Wigderson STOC 1997 Hardness versus randomness By a result of Impagliazzo and Wigderson (1997), at least one of the following two options is true: (i) EXP subset P/poly (ii) P=BPP The first statement says that every exponential time computable function can be computed using polynomial size circuits (for every separate input length). This is a very unlikely statement, that is strongly believed to be false, but alas, this is yet unproven. For example, it is believed that the famous NP-problem SAT requires superpolynomial circuits. The second statement says that every efficient randomized algorithm can be derandomized into an efficient deterministic algorithm. This is a very strong statement, that is partly backed by experience. Perhaps the most famous example is the problem of primality testing PRIMES, for which efficient randomized algorithms existed since the 1970, and that was eventually shown to be in P. However, there are still plenty of examples of randomized algorithms for which no good deterministic alternative exists. Still, given how unlikely (i) is, it is now believed that (ii) must be true. For this MFoCS project you can do the following: * Collect interesting examples of probabilistic algorithms for which no deterministic alternative is known. (E.g. polynomial identity testing (Schwarz-Zippel), estimating volumes using Monte Carlo methods.) * Understand part of the proof of the Impagliazzo-Wigderson result. There are several steps in the proof, that may be considered separately. The hardest part is the construction of a so-called pseudorandom generator (PRG). To derandomize a randomized algorithm, we need to deterministically generate random bits, which brings to mind the famous quote by John von Neumann: Anyone who attempts to generate random numbers by deterministic means is, of course, living in a state of sin. The PRG is a means to deterministically generate bits that look "random enough" to pull this off. Reference: L. Trevisan, Derandomization from hardness, 2019
Cynthia Kop C1: Rico te Wechel
Rewriting Induction + Linear Arithmetic = Decision Procedure Stephan Falke, Deepak Kapur IJCAR 2012 [slides] Rewriting induction is a proof method to show equivalence of equations using induction over a terminating term rewriting system. This paper describes the method of rewriting induction for term rewriting systems with integers, and gives a set of restrictions that guarantees that the proof method will always succeed in either proving equivalence or non-equivalence -- thus turning the method into a /decision procedure/. For the MFoCS project, there are several other papers on rewriting induction (with or without integers) that you could study as a second paper.
Kasper Hagens + Cynthia Kop C2: Adam Kjelstr&oshlash;m
Polynomial Invariants by Linear Algebra Steven de Oliveira, Saddek Bensalem, Virgile Prevosto ATVA 2016 [slides] When dealing with computer programming, one often wants to guarantee that the behavior of some piece of code coincides with its intended behavior. Methods from formal verification allow us to prove this. However, such proofs often depend on the availability of invariants. The paper presents a technique for generating polynomial invariants for while loops. This is done two steps: - Linearization: represent a while loop as a linear transformation. - Invariant generation: compute the polynomial invariants, using some linear representation.
Dario Stein D1: Dick Blankvoort
Generalising monads to arrows John Hughes Science of Computer Programming 37(1-3), 2000 John Hughes' *arrows* are an alternative formalism to monads for organizing effectful computation in functional programming. For every monad, functions `a -> m b` form an arrow, but not all arrows come from monads, so the arrow typeclass gives some extra generality at the expense of expressive power. This project is fairly open ended -- you'll begin with an introduction to arrows and why they can be useful. You can then dive deeper into implementations, or discuss the more mathematical aspects of arrows (premonoidal categories). It is interesting to compare the arrow interface with Haskell's `proc` notation and a graphical syntax such as string diagrams. Reading: You can learn about arrows in various places. The original arrows paper is "Generalising monads to arrows" (Hughes 2000), for more mathematical aspects, see "Arrows, like monads, are monoids" (Heunen&Jacobs 2006). For graphical notation, have a look at "String Diagrams for Premonoidal Categories" by Mario Roman. Topics: functional programming, category theory, graphical reasoning
D2: Sergio Domínguez Cabrera
Kan Extensions for Program Optimisation Or: Art and Dan Explain an Old Trick Ralf Hinze MPC 2012 In functional programming, `[x] ++ xs` has low complexity while `xs ++ [x]` is expensive. John Hughes' "difference lists" represent the list `xs` as the function `prep xs = (-) ++ xs`. Concatenation of difference lists then becomes function composition, which takes care of calling ++ in a more efficient order. This is an instance of a continuation-passing-style (CPS) translation. A generalized version of this trick starts with any monad M, and computes a more efficient continuation representation. Your project is to give an exposition of the continuation trick and an elementary tour of the relevant categorical concepts (monads, adjunctions, Kan extensions). The original paper uses an elegant graphical syntax to reason about these things, which you can present alongside functional programs, or even explore further with the graphical proof assistant Topics: category theory, graphical reasoning, functional programming
Niels van der Weide E1: Lean Ermantraut
Apartness, sharp elements, and the Scott topology of domain Tom de Jong MSCS 2023 Apartness is a fundamental notion in constructive mathematics. When we are working with objects that are inherently, such as real numbers or streams, then proving their equality requires infinite evidence. Apartness formulates inequality in a positive way, and proving apartness of a stream or a real number, only requires finite evidence. This notion is better behaved than equality constructively. This paper studies apartness from a constructive perspective using domain theory. Domain theory is a field of mathematics that has applications to theoretical computer science, programming languages, and topology, and the fundamental notion in domain theory is that of a dcpo It defines an intrinsic notion of apartness for dcpos, and it shows that this apartness relation is well-behaved if one restrict themselves to so-called sharp elements. In addition, the notion of strong maximality is defined, and it is shown that every strongly maximal element is sharp. The papers finishes with a number of examples, among which are the the Baire space (i.e., streams of natural numbers) and the Dedekind real numbers, and each of the aforementioned notion gets illustrated by them.
Freek Wiedijk F1: (not assigned)
Modular Verification of State-Based CRDTs in Separation Logic Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, Lars Birkedal ECOOP 2023 CRDTs are Conflict-free Replicated Data Types. These are datastructures for the case that people operate on data at different sites without continuous connectivity between those sites. The CAP theorem says that it is not possible to have simultaneously the properties of Consistency, Availability and Partition tolerance. Instead the property of strong eventual consistency is possible. These means that when the sites again get connected again, all sites eventually get into the same state without a need for manual conflict resolution, and furthermore ("strong") that the final state does not depend on the order in which the updates are communicated between the sites. Examples of applications of CRDTs are collaborative editors like Google Docs, and the shopping carts of online vendors. The paper (as well as an earlier paper in OOPSLA 2022) describes a formalization of the theory of CRTDs in Coq using the Iris framework. A presentation that just presents this theory clearly and mathematically already would be very nice. But looking at CRDTs for text editing (which can be quite complex) also is interesting.
F2: (not assigned)
Proving the Completeness Theorem within Isabelle/HOL James Margetson, Tom Ridge AFP 2004 First order predicate logic has two properties: it is sound and complete. Soundness means that provable statements hold in all models, and completeness states that statements that hold in all models are provable. This was the subject of Gödel's 1929 PhD thesis. This publication is not a refereed paper, but instead is a companion document for an Isabelle/HOL formalization of a proof of the completeness theorem. It might be interesting to compare this formalization with other completeness formalizations (possibly in other proof assistants). And it might be interesting to look into constructive versions of the completeness theorem.
F3: Finn van der Velde
ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, Jeremy Avigad arXiv 2023 Autoformalization is the use of machine learning and theorem proving to automatically turn existing mathematical texts in formalizations. The source for this might be latex (like for instance from arXiv), or scans of books or handwritten notes. The target then would be formalizations in systems like Coq, Isabelle or Lean. This is a very recent paper ("Under review"), which describes a benchmark for autoformalization in the context of the Lean system. A presentation that surveys the current state of the art of this field, as well as where things might be going, would be very interesting.
Herman Geuvers H1: Ioannis Koutsidis
Complete Bidirectional Typing for the Calculus of Inductive Constructions Meven Lennon-Bertrand ITP 2021 The article presents a so caled "bidirectional type system" for the Calculus of Inductive Constructions (CIC), which is the type theory of the Coq system. Type theory is about the typing judgement Γ ⊢ t : T, stating that term t is of type T in context Γ. The core of the Coq system is a "type checking algorithm" that verifies whether the judgment Γ ⊢ t : T holds. When developing atype checking algorithm, one immediately notices that one needs (simultaneously) a "type inference algorithm", which, given Γ and t, computes: either a T such that Γ ⊢ t : T holds, or `fail' to signify that no such T exists. So, a typung algorithm has two "modes", a "type checking" mode and a "type inference" mode. The bidirectional approach makes these two modes explicit in the typing rules, by decomposing the undirected typing Γ ⊢ t : T into two separate judgments Γ ⊢ t ▷ T (inference) and Γ ⊢ t ◁ T (checking). This decomposition allows a direct connection between the typing rules and the actual typing algorithms, but also gives a finer grained structure to typing derivations, which has independent interest. A key property of the bidirectional system is its completeness with respect to the usual undirected one. The bidirectional approach has become very popular and has been applied to various type theories. The present work applies it tothe type theory of Coq and proves its completeness, and all this has been formalised in Coq as a part of the MetaCoq project.
H2: Erika Xie
Normal Derivability in Classical Natural Deduction Jan von Plato, Annika Siders Review of Symbolic Logic 5(2), 2012 Following the Curry-Howard formulas-as-types correspondence, there is a one-one correspondence between natural deduction derivations (in logic) and typed lambda-terms. Moreover the reduction on these terms (e.g. beta-reduction) corresponds with so called "detour-elimination" on natural deduction. A central theorem states that this reduction terminates, which is an important result, as it implies that a derivable formula can be derived using a "normal derivation", which implies decidability of the logic. For intuitionistic logic, termination of detour elimination has been studied in detail, from various viewpoints (that is: using various definitions of the logical rules). So have the corresponding term reductions, which give rise to standard data-type operations. For classical logic, the situation has been less canonical for a long time: normalizability was only proven for fragments, or the proofs were really contrived. The paper by von Plato-Siders gives a concrete method to transform a derivation in classical predicate logic into normal-form. The 'trick' is that theu use so called "general elimination rules", which are not really described in the paper. (The paper is very concise anyway.) So it might be needed to also read at least sections 1,2 (and maybe also sections 5,6) of this paper: Natural deduction with general elimination rules -- Jan von Plato Archive for Mathematical Logic 40, 541–567 (2001)
Jurriaan Rot J1: Rutger Dinnissen
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. 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.
Loes Kruger + Jurriaan Rot J2: Cas Haaijman
Compositional Learning for Interleaving Parallel Automata Faezeh Labbaf, Jan Friso Groote, Hossein Hojjat, Mohammad Reza Mousavi FoSSaCS 2023 Automata learning is a family of techniques for automatically constructing automata by running tests, such as checking whether or not a word is in the target language. It has been applied, for instance, to learn models of - and find bugs in - implementations of network protocols. In this paper the authors assume structure on the target automaton, namely that it consists of several concurrent components. The idea is to learn these components, instead of the entire composed system (which is big). For this MFoCS project, you will learn about automata learning and this recent extension.
Marnix Suilen + Nils Jansen N1: (not assigned)
Predictive Representations of State Michael Littman, Richard Sutton, Satinder Singh NIPS 2001 Learning Predictive State Representations Satinder Singh, Michael Littman, Nicholas Jong, David Pardoe, Peter Stone ICML 2003 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 state of the environment, 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. Standard approaches to finding good decision-making strategies in POMDPs often consider the observation history. That is, a decision-making strategy looks back at what happened before in an attempt to gain knowledge about the current state of the environment. It is known, however, that no finite amount of history can ever be sufficient to fully identify the underlying state information of POMDPs in general. Predictive state representations (PSRs) were introduced for POMDPs as an alternative to histories. Instead of looking back at what happened before, a PSR looks ahead into the future and tries to predict what will happen. Formally, a PSR is a vector of predictions (probabilities) for a number of tests (finite sequences of actions and observations) that forms a sufficient statistic for the environment. In this project, we consider two papers as a starting point. Paper (1) connects POMDPs and PSR in a fundamental way by proving that every finite POMDP model has a linear PSR of size bounded by the number of POMDP states. When the POMDP model is fully known, a PSR can be constructed. However, in many realistic applications, POMDP models are unknown and need to be inferred from data. Paper (2) does precisely that by introducing an algorithm for learning a PSR from observed data from an unknown POMDP.
Eline Bovy + Nils Jansen N2: Willem Lambooij
Solving zero-sum one-sided partially observable stochastic games Karel Horák, Branislav Bošanský, Vojtěch Kovařik, Christopher Kiekintveld Artificial Intelligence 316, 2023 Partially Observable Stochastic Games (POSGs) are models for sequential decision-making problems with one or more players where the players have partial information about the state of the problem. POSGs extend the Partially Observable Markov Decision Processes (POMDPs) to the multi-agent setting. The goal in a POSG is to find a Nash equilibrium, i.e., decision-making strategies for each player such that no player can benefit by changing their strategy. This paper focuses on a subset of POSGs: two-player zero-sum one-sided POSGs. Zero-sum means that the players have directly opposing goals. A reward for one player leads to an equivalent negative reward for the other. One-sided means that only one of the players has partial observability while the other has full observability. The paper adapts the Heuristic Search Value Iteration algorithm (HSVI) used for POMDPs to work for their POSG subset. This algorithm approximates the expected discounted reward when both players play according to the Nash equilibrium. Furthermore, the paper provides algorithms to derive the approximate Nash equilibrium, so the decision-making strategies that lead to this expected discounted reward. Finally, the paper evaluates their new algorithms on various multi-agent sequential decision-making problems.
Robbert Krebbers R1: Daan Spijkers
Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq Enrico Tassi ITP 2019 When defining algebraic data types in programming languages such as Rust and Haskell one can let the language automatically generate boilerplate definitions. An example is the equality `T_eq : T → T → Bool`. Generating these definitions in proof assistants (such as Coq) instead of ordinary programming languages (such as Rust or Haskell) is complicated. One should also generate correctness proofs, e.g., `T_eq x y = true <-> x = y`. This paper addresses the challenge of dealing with containers (e.g., using `list` in the definition of n-ary trees) and providing modular proofs in the presence of Coq's syntactic termination checker. The result involves a technique called "unary parametricity" and has been implemented using the meta programming language "Coq-Elpi". Coq-Elpi is a new language based on "λProlog" that can be seen as a successor of Ltac. This paper will excite you if: - You want to understand how inductive types and termination checking works in type theory / Coq. - You want to know what "parametricity" is about - You want to learn about meta programming in in type theory / Coq. By reading a second paper you can, for example, study other uses of meta programming in Coq, study the theory of λProlog, investigate other challenges (types with many constructors, dependent types).
Ike Mulder + Robbert Krebbers R2: Menzo van Kessel
Subformula Linking for Intuitionistic Logic with Application to Type Theory Kaustuv Chaudhuri CADE 2021 Traditional proof systems for (intuitionistic) first-order logic have rules to manipulate a single connective in a single formula. This means that sometimes, it take quite a bit of effort to match hypotheses with your proof obligation. For example, suppose we are proving. ((A → A) → B ∧ C) ⊢ C ∧ B When proving this, you want to match up the atoms B and C from your hypotheses, with these same atoms in the goal. But to do so, you must first eliminate the implication (and prove (A → A)), then eliminate the conjunction, before you can continue. In a sense, these steps are quite 'mechanical'. This paper introduces 'subformula linking' for intuitionistic logic. Rather than doing all these steps yourself, you simply 'link' the occurrences of B in above example. The paper introduces rules that determine an appropriate remaining goal. There is a prototype tool, called ProfInt, so that you can actually do this in the browser. If you want to play around with it, see here: This paper should be interesting to you if you are interested in formal logic and automated or interactive theorem proving. For the second paper, you could look for example into earlier work on subformula linking in linear logic, or look into other work on 'gestural' theorem proving.
Marc Hermes + Robbert Krebbers R3: Jakob Wuhrer
Certifying Graph-Manipulating C Programs via Localizations within Data Structures Shengyi Wang, Qinxiang Cao, Anshuman Mohan, Aquinas Hobor OOPSLA 2019 [slides] Data structures frequently involve underlying graph elements, 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 complex pointer manipulations. The featured paper proposes a method grounded in a localization rule, enabling modular reasoning by focusing in on specific heap segments relevant to the program's execution. The papers listed in the accompanying slides present diverse approaches for verifying graph-based data structures, making them suitable for comparative analysis. "Proof Pearl: Magic Wand as Frame" stands out as an great primer on the subject.
Wieb Bosma W1: Sipho Kemkes
On the computational complexity of algebraic numbers: the Hartmanis-Stearns problem revisited Boris Adamczewski, Julien Cassaigne, Marion le Gonidec Transactions of the AMS 373(5), 2020 The paper is concerned with the question from computational complexity theory asking how difficult it is to compute the base b digits of an algebraic real number. In this nicely written, recent paper three negative results are proven, two of which are novel. They state that it is impossible to generate the base b expansion * by a finite automaton (or uniform morphism), or * by a morphism with exponential growth, or * by a deterministic pusdown automata. As a consequence, real numbers generated by either of these devices are necessarily transcendental (if not rational). It may not be necessary to master all the details of this long paper, but you should certainly acquire the taste of results and proofs. For a second paper it may be useful to go back to either the paper of Hartmanis and Stearns, or probably better, to the paper by Cobham that appeared a few years later and in which he proved the first result (apparently) and also stated the second result.