Bachelor- und Masterarbeiten

The Lean theorem prover is built on a fairly minimal core type theory. By design, Lean itself is not particularly trustworthy (e.g. it allows users to circumvent its type system in ways that are hard to detect), but it can export finished proofs, which are terms of the core type theory. These can then be checked by small, trustworthy third-party checkers (1, 2, 3).

The aim of this project is to build one such checker (though we may limit the scope to a subset of the core type theory). To do so, you'll have to familiarise yourself with the rules of the core type theory and then define its abstract syntax and write a parser and typechecker.

Familiarity with basic compilation techniques (parsing, abstract syntax, typechecking) is required. Experience with dependent type theories would be very helpful. The project is suitable for a master or strong bachelor student.

The Lean theorem prover has a very flexible parsing mechanism which allows us to embed other languages into it. In this project, we'd like to use this mechanism to embed intensional or extensional Martin Löf type theory. This means you'll have to define the abstract syntax and type system of this type theory in Lean and write a parser type checker for it. (We aim to use the embedded type theory to simplify proofs about its categorical models.)

A solid command of functional programming is required, as is familiarity with basic compilation techniques (parsing, abstract syntax, typechecking). Experience using theorem provers based on dependent type theory (e.g. Agda, Coq, Lean) would be very helpful. The project is suitable for a master or strong bachelor student.

Lifting is a technique to produce hard instances of CNF formulas from easier ones. In a recent paper [1], a lower bound for proofs of certain lifted formulas in the regular resolution proof system was shown. For these formulas, upper bounds in a stronger proof systems related to clause learning [2] should be derived.

[1] Vinyals, Elffers, Johannsen, Nordström, "Simplified and Improved Separations between Regular and General Resolution by Lifting", SAT 2020

[2] Buss, Hoffmann, Johannsen, "Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL-Algorithms with Clause Learning", LMCS 4, 2008.

In the Lean theorem prover, some tasks, such as proving the continuity of a function or a linear inequality, can be automated by using some sort of specific strategy. For example, the `continuity` tactic uses a general theorem prover restricted to some set of lemmas that concern continuity to complete a goal.

This project aims to improve existing specialised tactics available in Mathlib or create new ones that would solve particular types of goals.

To tackle this project, you will have to familiarise yourself with some of the metaprogramming APIs of Lean, for which a solid command of functional programming, including monads, is required. Experience with theorem provers based on dependent type theory (e.g. Agda, Coq, Lean) would be helpful.

This type of thesis aims to define and then prove some interesting properties about a mathematical concept, system, structure, or implementation, using Isabelle [1], Lean [2], or HOL4 [3]. There exists a wide variety of possible formalization projects; you may either come to us with an idea of your own, or we look for one in a field that interests you.

For a project like this, prior experience with Isabelle, Lean, or HOL4 (or another proof assistant like Coq or Agda) is very helpful but not strictly required if you are willing to learn to use them in the process. For Master's level, due to the probable scope of the project, not having prior experience might prove to be challenging, though.
Resources: Lean 4 learning material, Isabelle Tutorial, Concrete Semantics with Isabelle/HOL, Functional Data Structures and Algorithms, HOL4 Tutorial and Documentation.

[1] https://isabelle.in.tum.de/
[2] https://lean-lang.org/
[3] https://hol-theorem-prover.org/

Some interesting projects:

Verification of homework sheets:

We would like to find out how viable and helpful it is to verify homework sheets (e.g. for the lecture "Logik und diskrete Strukturen"). Also possible automations can be explored.

Verified Ordered Resolution:

We verified the Superposition Calculus for first order logic using the Saturation Framework in Isabelle. The same verficiation strategy could be also applied to verify Ordered Resolution for first order logic.

Diff-Arrays:

Functional lists are a convenient and easy-to-use data structure in functional programming. However, compared to imperative arrays, lookup and update operations on lists have a significantly worse runtime of O(n) instead of O(1). For this reason, we created an automatic refinement of linearly used lists to arrays and also non-linearly used lists to diff arrays. Diff arrays are persistent and store their updates in a tree-like structure next to a plain array. With them, we can have lookup and update operations in O(1) for its most recent version. Parallel to the refinement, we will automatically create equivalence proofs using the Isabelle/HOL theorem prover and its Imperative/HOL and separation logic facilities to ensure that the two versions of the program are doing the same.
Repository
In the future work chapter of this thesis, you can see the open tasks in this endeavor. All four tasks described there would give a good entry point to a Master's or Bachelor's thesis.

Functional Real-Time Deque:

Based on the work of Chuang and Goldberg, we implemented and formally verified a double-ended queue (deque) in a purely functional language such that each enqueue and dequeue operation on either end takes O(1) time in the worst case. This is what real-time means. Operations on previous versions of a deque are in constant time since purely functional data structures are persistent by default.
Paper: https://drops.dagstuhl.de/opus/volltexte/2023/18404/pdf/LIPIcs-ITP-2023-29.pdf
Entry in the AfP: https://www.isa-afp.org/entries/Real_Time_Deque.html

However, we do not support the catenation of deques. This paper by Kaplan and Tarjan describes a fully functional implementation of a real-time deque with catenation: https://dl.acm.org/doi/abs/10.1145/324133.324139
We found an actual implementation of it in OCaml: https://github.com/art-w/deque
A good entry point to your Master's or Bachelor's thesis could be re-implementing this data structure in a functional programming language of your choice and comparing it to the Deque implementation without catenation based on Chuang and Goldberg.

The tooling of theorem provers is often lagging behind compared to main stream programming languages. Improvements are always welcome. This is also the case for Isabelle.

Some interesting projects:

AI Search

It is often tedious to find out if certain theorems already exist in the Isabelle Library or the Afp. An AI search tool could be helpful!

jEdit Dark mode

jEdit, the main IDE for Isabelle, does not/just partially support dark mode: Dive into the rendering options of Isabelle and create new, consistent and good-looking color schemes. (Also the options menu in general could use a rework.)

Isabelle minted

Improve support for Isabelle in the minted Latex package.

Improve Visual Studio Code Plugin

Better than improving jEdit would be to fully replace it by Visual Studio Code. The VS Code Plugin for Isabelle needs some improvements though.

Open projects in jEdit

Often Isabelle projects cannot be opened from within jEdit, because they need some CLI Arguments. Add this functionality.

Aesop is a proof search tool developed by Jannis Limperg and Xavier Généreux for the Lean 4 theorem prover. It runs various Lean tactics in an attempt to automatically find proofs of 'trivial' propositions. Currently, these tactics perform type-level computations, which are a core feature of Lean's type system, lazily, i.e. only when such computations are necessary. This has generally been found to be the most efficient way to implement Lean and similar theorem provers.

However, in the context of Aesop, we often operate on the same or very similar expressions multiple times, so it may be more efficient to perform all type-level computations at once (i.e., to normalise the expressions). Additionally, normalisation would allow us to use a variety of techniques from automated theorem proving, e.g. very efficient indexing methods. Hence the goal of this project is to implement eager normalisation (and possibly some follow-up optimisations) and to evaluate whether this indeed increases Aesop's performance.

Cyber-physical systems combine computation and physical behavior, e.g. airplanes, nursing robots, and (autonomous) vehicles. Due to their frequent and close interaction with humans, their correct behavior is of utmost importance. Malfunctions may even endanger humans life and health. Logic and theorem proving can help to analyze the correctness of cyber-physical systems, e.g. safety properties can be proven formally. In this area, I offer various topics on the formalization of such logics and their implementation as theorem prover micro-kernels. For current topics, see Marvin Brieger's home page.