If you are interested in a topic for a thesis, please contact Prof. Smolka or a researcher of the Lab whose work you find interesting.
As part of your thesis work, you will participate in our Graduate Seminar. You will give two talks in your seminar phase and one final talk after submitting your thesis. The first and second talk are 15 minutes each, the final talk is 20 minutes, always plus discussion time.
When you start your thesis work, your advisor will provide you with a problem specification (1 page). You will maintain a web page devoted to your thesis work. The problem specification, the thesis and related software and documentation will be made available through this page (see examples below).
Niklas Mück, 2022,
The Arithmetical Hierarchy and Post’s Theorem in Coq
(Advisors: Forster and Kirst)
Benjamin Peters, 2022,
Computational Proofs of Gödel's First Incompleteness Theorem in Coq
(Advisor: Kirst)
Adrian Dapprich, 2021,
Generating Infrastructural Code for Terms with Binders using MetaCoq
(Advisor: Dudenhefner)
Johannes Hostert, 2021,
The Undecidability of First-order Logic over Small Signatures
(Advisors: Kirst and Dudenhefner)
Nils Lauermann, 2021,
A Formalization of Kolmogorov Complexity in Synthetic Computability Theory
(Advisor: Kunze)
Mark Koch, 2021,
Mechanization of Second-order Logic
(Advisor: Kirst)
Christian Hagemeier, 2021,
Formalizing Intuitonistic Epistemic Logic in Coq
(Advisors: Kirst and Sturm)
Felix Jahn, 2020,
Synthetic One-One, Many-One, and Truth-Table Reducibility in Coq
(Advisor: Forster)
Marcel Ullrich, 2020,
Generating induction principles for nested inductive types in MetaCoq
(Advisor: Forster)
Lennard Gäher, 2020,
Towards a Formal Proof of the Cook-Levin Theorem
(Advisor: Kunze)
Dominik Wehr, 2019,
A Constructive Analysis of First-Order Completeness Theorems in Coq
(Advisors: Kirst, Forster)
Simon Spies, 2019,
Formalising the Undecidability of Higher-Order Unification
(Advisor: Forster)
Sarah Mameche, 2019,
Strong Normalization of the Lambda Calculus in Lean
(Advisor: Stark)
Daniel Freiermuth, 2018,
Formalizing Stream Calculus in Coq
using Causality and Prefix Equality
(Advisor: Schäfer)
Maximilian Wuttke, 2017,
Verified Programming of Turing Machines in Coq
(Advisor: Forster)
Leonhard Staut, 2017,
Nu-Trees in Coq: Their Language and Automata
(Advisor: Kirst)
Edith Heiter, 2017,
Undecidability of the Post Correspondence Problem in Coq
(Advisors: Forster and Smolka)
Felix Rech, 2017,
Strictly Positive Types in Homotopy Type Theory
(Advisor: Schäfer)
Julian Tobias Rosemann, 2017,
Formal Verification of a Family of Spilling Algorithms
(Advisor: Schneider)
Joachim Bard, 2017,
A Formal Completeness Proof for PDL
(Advisor: Doczkal)
Lukas Convent, 2016, won
FdSI-Bachelor-Preis,
Compositional and Nameless Formalization of HOcore
(Advisor: Tebbi)
Jana Hofmann, 2016,
Verified Algorithms for Context-Free Grammars in Coq
(Advisor: Smolka)
Jan Menz, 2016,
won
FdSI-Bachelor-Preis,
A Coq Library for Finite Types
(Advisor: Smolka)
Fabian Kunze, 2015,
won
FdSI-Bachelor-Preis,
Verified Compilation of Weak Call-by-Value Calculus to Combinators
and Closures
(Advisor: Smolka)
Clara Schneidewind, 2015,
won
FdSI-Bachelor-Preis,
Regularity and Linearization of Tail-Recursive Programs
(Advisor: Smolka)
Alexander Anisimov, 2015,
Proof Automation for Finite Sets
(Advisor: Doczkal)
Denis Müller, 2015,
A Syntactic Theory of Finitary Sets
(Advisor: Schäfer)
Yannick Forster, 2014,
won
FdSI-Bachelor-Preis,
A Formal and Constructive Theory of Computation
(Advisor: Smolka)
Dominik Kirst, 2014,
Formalization of Zermelo's Well-Ordering Theorem
(Advisor: Kaiser)
Jonas Oberhauser, 2013,
Termination and Confluence of CC
(Advisor: Brown)
Jan-Oliver Kaiser, 2012,
Constructive Formalization of Regular Languages
(Advisors: Doczkal and Smolka)
Gilles Nies, 2012,
Representations of Boolean Functions in Constructive Type Theory
(Advisor: Brown)
Andreas Teucke, 2011,
Translating a Satallax Refutation to a Tableau Refutation Encoded in Coq
(Advisor: Brown)
Tobias Tebbi, 2011,
won
FdSI-Bachelor-Preis,
Correctness of Tableau-Based Decision Procedures
with Backjumping
(Advisors: Kaminski, Smolka)
(won FdSI-Bachelor-Preis)
Carsten Hornung, 2011,
Constructing Number Systems in Coq
(Advisors: Brown, Smolka)
Matthias Höschele, 2009,
Towards a Semiautomatic
Higher-Order Tableau Prover
(Advisors: Brown, Smolka)
Sigurd Schneider, 2009,
Terminating Tableaux for Modal Logic with Transitive Closure
(Advisors: Kaminski, Smolka)
Julian Backes, 2008,
A database of higher-order problems (Advisor: Brown)
Xin Zhang, 2007-2008,
An M-Set Model of Higher Order Abstract Syntax
(Advisor: Brown)
Raphael Reischuk, 2008,
won
FdSI-Bachelor-Preis,
Reconciling Copying and Trailing for Constraint Programming Systems
(Advisor: Tack)
(won FdSI-Bachelor-Preis)
Esfandiar Mohammadi, 2007,
On the Category of Stratified Coherence Spaces
(Advisor: Schwinghammer)
Jochen Setz, 2007,
A Principle Compiler for Extensible Dependency Grammar
(Advisor: Debusmann)
Christian Doczkal, 2007,
Proof-theoretic Aspects of Call-by-push-value Calculus
(Advisor: Schwinghammer)
(won FdSI Bachelor Award)
Dieter Brunotte, 2006,
Subtyping and Computational Monads
(Advisor: Schwinghammer)
Andi Scharfstein, 2006,
A Sandboxing Infrastructure for Alice ML
(Advisor: Rossberg)
Georg Neis, 2006,
A Semantics for Lazy Types
(Advisor: Rossberg)
Moritz Hardt, 2006,
Hybrid Logic Revisited
(Advisor: Smolka)
Dominik Brill, 2006,
Constraint Programming in Alice. A Tutorial.
(Advisor: Tack)
Patrick Pekczynski,
2005,
Implementation and Evaluation of
Advanced Propagation Algorithms for
Global Constraints
(Advisor: Tack)
Simon Georg Pinkel,
2004,
Alice Server Pages
(Advisor: Tack)
Niko Paltzer, 2005,
Efficient Representation of Dynamic Types.
(Advisor: Rossberg)
Christian Hümbert, 2005,
A Proof Assistant for Higher-order Predicate Logic
(Advisor: Smolka)
Mark Kaminski, 2005,
Studies in Higher-order Equational Logic
(Advisor: Smolka)
Matthias Berg,
2004,
Polymorphic Lambda Calculus with Dynamic Types
(Advisors: Smolka,
Tack)
Marvan Odeh,
2004,
Modellierung natürlicher Sprachen mit Hilfe von TDG
(Topologische Dependenzgrammatik)
(Advisor: Debusmann)
Christian Müller,
2004,
Interpreter für getypte Lambda-Kalküle
(Advisors: Tack,
Smolka)
Mathias Möhl,
2004,
Modelling Natural Language with
Topological Dependency Grammar
(Advisor: Debusmann)
Robert Grabowski,
2003,
Eine GTK-Schnittstelle für Alice
(Advisors: Brunklaus,
Rossberg)
Bernadette Blum and
Marvin Schiller,
2003,
Ein Browser für Alice
(Advisor: Brunklaus,
Rossberg)
Jens Regenberg, 2003,
Ein Debugger für die Alice VM
(Advisors: Brunklaus,
Kornstaedt)
Matthias Horbach
and Sven Woop,
2002,
Effiziente Datenstrukturen für Lambda-Bäume
(Advisor: Smolka)
Dainius Ramanauskas,
2002,
Bibliothekssystem der Computerlinguistik
(Advisor: Schulte)
Guido Tack,
2002,
Integrated Oz Search Factory
(Advisor: Schulte)
Jan Schwinghammer,
2002,
Jacke: A Parser-Generator Tool for Standard ML
(Advisors: Kornstaedt,
Rossberg)
Marco Kuhlmann,
2001,
Tiny Constraint Modelling Language
(Advisor: Schulte)
Martin Homik,
1999,
JOz: Grafisches Java-Oz Frontend
(Advisor: Schulte)