Available Projects & Theses
General Information
Our projects and theses are focused on the design and implementation of programming languages, functional and object-oriented programming, type systems and static analysis, semantics, concurrency, mechanized metatheory, and theorem proving.
If you are interested in one of the topics below or you have a specific topic in mind yourself please write an email to Prof. Dr. Thiemann.
This page is a living document and we may not always be able to update it in time. Some topics may already be taken and others might not yet have found their way onto here. If you are interested in a project or thesis with our chair but cannot find a suitable topic feel free to write an email to as well and let us know which of the specialization courses offered by our chair you have taken.
Bachelorprojekt
Extensions to the compiler construction lecture compiler
- Arrays
- Strings / Chars
- Match
- …?
Extending Lambda Pi Paper with Universe Polymorphism
- Addition of universe levels and polymorphism to the existing implementation
- The type checker would use the subtype approach suggested here:
https://github.com/agda/agda/issues/5810, where
Set l<Setωfor alll. - as project: implementation
- follow up with thesis: proof, maybe explore alternatives, build upon Hannes’ dependent types formalization
Bachelorarbeit
Master Lab Course
Master Project
Extensions to the compiler construction lecture compiler
call/ccshift/reset- generators
Register Allocation using SAT Solving
- Usage of the compiler from the lecture
- Translation of the graph coloring problem to SAT
- Interfacing with an existing SAT solver (e.g. KISSAT, CaDiCaL)
- (Fuzzer based) Generation of large program instances to produce reasonable benchmarks for both runtime and compilation speed
Use agda-hs for program extraction of existing correct algorithm
- students must be comfortable adjusting the Agda code to fit the custom agda-hs prelude
Reproduce Agda proofs in Lean
- SystemF or Logical Rel.
- Possible research questions:
- What is a good representation for syntax (extrinsic; scoped; intrinsic)?
- How do we represent substitutions?
- What can Lean solve automatically, what Agda cannot?
- What libraries exist to formalize PLs in Lean?