Title: Synthetic computability and undecidability
Chair: Thomas Somers
Advisor: Anton Golov
Bauer, Andrej. "First steps in synthetic computability theory." Electronic Notes in Theoretical Computer Science 155:5-31, 2006.
Forster, Yannick et al. "On synthetic undecidability in Coq, with an application to the Entscheidungsproblem." Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019.
Abstract:
Computability theory traditionally reasons about computable functions and sets using Gödel encodings and models of computation, such as Turing machines. Synthetic computability works in a constructive mathematical universe where all sets and functions have computability structure. This allows us to talk about computability while avoiding Gödel encodings and models of computation entirely. In this setting, proving undecidability is not possible without adding additional axioms. This can be resolved by reducing to a known undecidable problem, such as Post's correspondence problem (PCP). We discuss some of the basic results that have been proved in this context, how this is formalized in Coq, and how reduction to PCP can be used to prove undecidability.
Title: Representing partial computable functions in lambda calculus
Chair: Jelmer Firet
Advisor: Bas Terwijn
Henk Barendregt. Theoretical Pearls: Representing 'undefined' in lambda calculus. Journal of Functional Programming, 2(3), 367-374, 1992.
Albert Visser. Numerations, λ-calculus & arithmetic. To HB Curry: essays on combinatory logic, lambda calculus and formalism, 259-284, 1980.
Abstract:
A p.c. function psi is represented by a lambda term F if
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.
Title: Tropical Geometry of Deep Neural Networks
Chair: Kirsten Hagenaars
Advisor: Marnix Suilen, Nils Jansen
Zhang, Liwen, Gregory Naitzat, and Lek-Heng Lim. "Tropical geometry of deep neural networks." International Conference on Machine Learning. PMLR, 2018.
Morrison, Ralph. "Tropical geometry." A Project-Based Guide to Undergraduate Research in Mathematics. Birkhäuser, Cham, 63-105, 2020.
Abstract:
There are explicit connections between tropical geometry and feedforward neural networks with ReLU activation. The family of such neural networks is equivalent to the family of tropical rational maps. In the first part of my presentation I will give an introduction to tropical algebra and tropical geometry. In the second part of the presentation I will introduce neural networks, and a connection will be established between tropical geometry and multilayer neural networks. Finally, I will analyze neural networks with tropical tools, which shows that tropical algebraic geometry tools can be used to provide insights on neural networks.
Title: Bisimilarity Distances
Chair: Tjitske Koster
Advisor: Nils Jansen, Marnix Suilen
Bacci, G., Bacci, G., Larsen, K. G., & Mardare, R. Computing behavioral distances, compositionally. In International Symposium on Mathematical Foundations of Computer Science (pp. 74-85). Springer, Berlin, Heidelberg. August 2013.
Amortila, P., Bellemare, M. G., Panangaden, P., & Precup, D. Temporally extended metrics for markov decision processes. In SafeAI@AAAI. January 2019.
Abstract:
When it comes to analysing processes, methods to compare the behaviour of separate processes are often useful. These papers introduce two different methods for determining similarity between processes, specifically Markov Decision Processes, and for one of them an algorithm is proposed to calculate this measure of similarity. Moreover, a method for making this algorithm more efficient by composing smaller processes together is discussed, as well as conditions on the manner of composing that must be met in order to ensure similarity is preserved upon composing.
Title: Generating low-level code from high-level code for fast and verified programs
Chair: Pavel Zwerschke
Advisor: Ike Mulder, Robbert Krebbers
Clément Pit-Claudel, Jade Philipoom, Dustin Jamner, Andres Erbsen, and Adam Chlipala. Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2022). Association for Computing Machinery, New York, NY, USA, 918-933, 2022.
Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy. Verified low-level programming embedded in F*. Proc. ACM Program. Lang. 1, ICFP, Article 17, 29 pages, September 2017.
Abstract:
In some application domain, like cryptography, code needs to be very fast as well secure. In an ideal world there would be a clear-cut programming language of choice that produces code which excels at both. In practice however, high-level languages that are easy to reason about, e.g. Coq, tend to produce slower code than handwritten code in a low-level language like C. In order to gain the best of both worlds, this issue can be solved by writing equivalent code in a high-level and a low-level languages and then manually proving their equivalence. However, this can be a tedious and error-prone process. This talk introduces two approaches that try to help automate this process. The first approach introduces the concept of relational compilation and an implementation of this concept in the compiler construction toolkit Rupicola. Rupicola provides an extensible way of compiling Coq to C that keeps correctness intact. The second approach introduces Low*, a DSL within the high-level language F* that models C, and KaRaMeL, which compiles Low* to C. This way a programmer has both fine-grained control over memory as well as the power of F* for proofs and specifications.
Title: Translating Control Flow Graphs using Dominator Trees
Chair: Niek Terol
Advisor: Jules Jacobs, Robbert Krebbers
Ramsey, Norman. "Beyond Relooper: recursive translation of unstructured control flow to structured control flow (functional pearl)." Proceedings of the ACM on Programming Languages 6. 1-22, ICFP 2022.
Lengauer, Thomas, and Robert Endre Tarjan. "A fast algorithm for finding dominators in a flowgraph." ACM Transactions on Programming Languages and Systems (TOPLAS) 1.1: 121-141, 1979.
Abstract:
Control flow graphs can be used to visualize a program flow. Let's do the opposite and generate program code from control flow graphs. The main paper dealt with generating the low-level intermediate code WebAssembly. In this presentation, we will instead focus on a simpler representation of this code. The challenge was to preserve the semantics of the control flow and not insert any additional or duplicate code. We will go through some examples and introduce concepts that can help us solve that problem. In particular, we will look at dominator trees, which have some useful properties for preserving program flow. We will discuss an algorithm that computes the dominator tree and finally the algorithm that uses this tree to translate the control flow.
Title: Generalized rewriting in Coq
Chair: Alex van der Hulst
Advisor: Jules Jacobs, Robbert Krebbers
Sozeau, M., Oury, N. First-Class Type Classes. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2008. Lecture Notes in Computer Science, vol 5170. Springer, Berlin, Heidelberg, 2008.
Sozeau, M. A New Look at Generalized Rewriting in Type Theory. Journal of Formalized Reasoning, 2(1), 41-62, 2009.
Abstract:
Rewriting is a powerful mechanism in Coq.
Whenever we have a assumption H : x = y, we can use various tactics to rewrite this equation in the proof context.
This if easier than using the induction principle of equality explicitly.
With the use of generalized rewriting, the user can also rewrite using other relations than equality.
For example, one can rewrite a logical equivalence (P <-> Q) to change the goal.
Furthermore, the user can even rewrite with relations they defined themselves.
For example, if they have defined congruence modulo k, have an assumption H : a = b mod k,
and have shown that (P : nat -> Prop) is well-defined modulo k, they can use rewrite H to transform the goal from P a to P b.
In this talk we start by discussing type classes in Coq.
They are an essential building block for generalized rewriting.
In the second part, we discuss the generalized rewriting mechanism, with a primary focus on how to use it.
Title: Later Credits: Reducing the Proof Cost of Step-Indexing in Iris
Chair: Astrid van der Jagt
Advisor: Robbert Krebbers
Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. Later Credits: Resourceful Reasoning for the Later Modality. Proc. ACM Program. Lang. 6, International Conference on Functional Programming, Article 100. August 2022.
Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, Volume 28, e20. 2018.
Abstract:
In recent years, step-indexed separation logics such as Iris have become
essential tools for modelling modern, richly typed languages and reasoning about
concurrent programs.
In particular, step-indexed logical relations have proven to be highly suited
for modelling languages with "cyclic" features, such as recursive subtyping and
higher-order state. A key abstraction for step-indexed reasoning is the
so-called later modality (▹). In order to access and use a proposition ▹P
guarded by the later modality, the later must be eliminated, which can pose
quite a challenge in certain cases.
After a brief look at Iris and step-indexing, we will discuss a new technique for dealing with this later elimination problem: Later credits, which can be "saved up" and redeemed within a proof to eliminate a later, facilitating a form of amortised step-indexed reasoning which enables simpler and more intuitive proof patterns as well as new, previously unfeasible proofs.
Title: Objecs of categories as complex numbers
Chair: Daniël van Leijenhorst
Advisor: Dario Stein
M. Fiore and T. Leinster, Objects of categories as complex numbers, 2004.
M. Fiore, T. Leinster, An objective representation of the Gaussian integers, 2004.
A. Blass, Seven trees in one, 1995.
Abstract:
We solve the equation T=1+T^2 with complex T to see T^6=1, therefore T^7=T. If we now see T as a tree instead of a complex number we have an isomorphism from seven trees into one. This looks like a nonce argument, since trees are not complex numbers, but it appears to be a valid proof. We can even broaden this to see that if an equation holds for complex numbers then it holds in all distributive categories. There are some restrictions on the equations as we will see (note that there is of course no isomorphism from six trees into one node). We will look at the restrictions, give a proof and some examples.
Title: Automata Learning
Chair: Gerbrich Kroon
Advisor: Jurriaan Rot
Borja Balle and Mehryar Mohri, Learning Weighted Automata, 2015.
Takamasa Okudono, Masaki Waga, Taro Sekiyama, Ichiro Hasuo, Weighted Automata Extraction from Recurrent Neural Networks via Regression on State Spaces, 2019.
Abstract:
The field of automata learning focusses on inferring the model of a system by observing its behaviour. Angluin's L* algorithm has been dominating the field of automata learning, it learns a Deterministic Finite Automaton by asking so-called equivalence and membership queries to a Minimally Adequate Teacher. The L* algorithm can be extended to learning Weighted Finite Automata. This allows for learning the model of a system which outputs real values (or some other field) . For example, we can extract a Weighted Finite Automaton from a Recurrent Neural Network using this extension of the L* algorithm. This allows for easier analysis of the Recurrent Neural Network and faster inference.
Title: Defining natural numbers in type theory
Chair: Marten Straatsma
Advisor: Herman Geuvers
Steve Awodey, Jonas Frey, and Sam Speight. "Impredicative Encodings of (Higher) Inductive Types". In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. LICS '18. Oxford United Kingdom: ACM, July 9, pp. 76-85, 2018.
Ivar Rummelhoff. "Polynat in PER Models". In: Theoretical Computer Science 316.1-3, pp. 215-224, May 2004.
Abstract:
We would like to define inductive types in Type Theory. The type polynat ≡ ∀X. (X → X) → X → X is a good candidate for the type of natural numbers. However, there exists a model of polymorphic lambda calculus where not all elements of polynat are church numerals. As a result there is no unique recursor, which is required to define induction. We will look at a refinement of polynat that guarantees a unique recursor which can be proven within the type system.
Title: Algebraic Linearity of the Linear Lambda Calculus
Chair: Sander Suverkropp
Advisor: Herman Geuvers
A. Díaz-Caro and G. Dowek, "Linear lambda-calculus is linear," Leibniz International Proceedings in Informatics, LIPIcs, vol. 228, 21:1-21:0, 21 2022.
L. Vaux, "The algebraic lambda calculus," Mathematical Structures in Computer Science, vol. 19, no. 5, pp. 1029-1059, 2009.
Abstract:
In linear logic, all variables have to be used exactly once. The name linear logic, suggests that the logic is related to algebraic linearity. The linear lambda calculus is an extension of linear logic with addition and scalar multiplication. In this calculus, we can express vectors and matrices as terms of specific types. Using these, we discuss how all linear functions can be expressed as proofs, and that all proofs to vector types are algebraically linear. Finally, we will discuss another extension of linear logic, in which the linearity is enforced by an algebraic equality on terms. For this extension, we will briefly discuss the important normalization properties.
Title: On Non-Looping Term Rewriting & Proving Non-Looping Non-Termination Automatically
Chair: David Läwen
Advisor: Cynthia Kop
Wang, Yi, and Masahiko Sakai. "On non-looping term rewriting." Proceedings of the 8th International Workshop on Termination (WST'06), 2006.
Emmes, Fabian, Tim Enger, and Jürgen Giesl. "Proving non-looping non-termination automatically." International Joint Conference on Automated Reasoning. Springer, Berlin, Heidelberg, 2012.
Abstract:
In this talk we will discuss Term Rewrite Systems. First, we will recap what they are and talk about termination. The usual method for proving non-termination is to find looping reduction sequences. However, there are non-looping infinite reduction sequences. We will look at a few examples and discuss definitions for inner-looping and normal sequences. Next, we will consider a technique to prove non-termination of Term Rewrite Systems automatically, which is able to detect non-looping non-termination by generating pattern rules of the Term Rewrite System. The pattern rules represent a whole set of rewriting sequences. The pattern rules are narrowed until a rule is detected that is obviously non-terminating.
Title: Proving termination using the dependency pair method and SAT
Chair: Simcha van Collem
Advisor: Cynthia Kop
Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., & Zankl, H. SAT solving for termination analysis with polynomial interpretations. In International Conference on Theory and Applications of Satisfiability Testing (pp. 340-354). Springer, Berlin, Heidelberg. May 2007.
Hirokawa, N., & Middeldorp, A. Tyrolean termination tool: Techniques and features. Information and Computation, 205(4), 474-511. 2007.
Abstract:
The dependency pair method is a strong tool for proving termination of term rewrite systems. We discuss refinements that increase the proving power and efficiency of this method, such as the use of the dependency graph and projections. We furthermore show how to encode polynomial interpretations as a SAT problem and how to add the possibility of negative constant coefficients.
Title: Extensions of CompCert
Chair: Christoph Hoffmeyer
Advisor: Freek Wiedijk
Yuting Wang, Pierre Wilke, and Zhong Shao, An abstract stack based approach to verified compositional compilation to machine code, POPL 2019.
Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, and Viktor Vafeiadis, Lightweight verification of separate compilation, POPL 2016.
Abstract:
In this talk, two extensions of CompCert will be presented. CompCert is a verified compiler for the programming language C. A verified compiler is a compiler for which it is proven that the generated code is semantically equivalent to the source code. CompCert is only able to compile whole programs, i.e. programs consisting of a single file. The first extension, SepCompCert, improves CompCert so that it is able to compile programs consisting of multiple files. CompCert also assumes that it has access to an infinite stack. The second extension, Stack-aware CompCert, alters CompCert so that it is aware of its stack usage.
Title: Decidability of string graphs
Chair: Aron van Hof
Advisor: Wieb Bosma
Marcus Schaefer, Daniel Štefankovič, Decidability of string graphs, Journal of Computer and System Sciences, Volume 68, Issue 2, 2004.
Jan Kratochvíl, Jiří Matoušek, String graphs requiring exponential representations, Journal of Combinatorial Theory, Series B, Volume 53, Issue 1, 1991.
Abstract:
Consider a collection of curves. A string graph is a graph isomorphic to the intersection graph of this collection of curves. In this talk, we will derive a proof for the decidability of the string graph problem, i.e., for a given graph G, is there a collection of curves s.t. their intersection graph is isomorphic to G? We show that this can be decided in nondeterministic exponential time. In the second part of my talk, I give an example for a graph which has >= 2^(c*n) intersections where n is the number of vertices of this graph.
[link to the old page with descriptions of the projects by the teachers]