If you are interested in a topic for a thesis, please contact Prof. Smolka.
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 work out with you a problem specification. 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).
Haoyi Zeng, 2024,
Post's problem and the Priority Method in Synthetic Computability
(Advisors: Forster and Kirst)
Janis Bailitis, 2024,
Löb's Theorem and Provability Predicates in Coq
(Advisors: Forster and Kirst)
Fabian Brenner, 2024,
The Undecidability of Contextual Equivalence on PCF2 - Towards a Mechanisation in Coq
(Advisors: Forster and Kirst)
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,
won FdSI-Bachelor-Preis
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,
won FdSI-Bachelor-Preis
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,
won FdSI-Bachelor-Preis
A Constructive Analysis of First-Order Completeness Theorems in Coq
(Advisors: Kirst, Forster)
Simon Spies, 2019,
won FdSI-Bachelor-Preis
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)
Maxi 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)
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, 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)
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,
won FdSI-Bachelor-Preis
Proof-theoretic Aspects of Call-by-push-value Calculus
(Advisor: Schwinghammer)
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)