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 20 minutes each, the final talk is 30 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).
Hizbullah Abdul Aziz Jabbar, 2022,
Mechanized Undecidability of Halting Problems for Reversible Machines
(Advisor: Dudenhefner)
Roberto Álvarez Castro, 2022,
Undecidability of subtyping in System F
(Advisor: Forster)
Marc Hermes, 2021,
On First-Order Arithmetic in Coq
(Advisors: Kirst and Weber)
Felix Rech, 2020,
Mechanizing Set Theory in Coq: The Generalized Continuum Hypothesis and the Axiom of Choice
(Advisor: Kirst)
Moritz Lichter, 2017
Decidability of S1S in Constructive Type Theory
(Advisor: Smolka)
Sigurd Schneider, 2013,
won
Günther-Hotz-Medaille,
Semantics of an Intermediate Language for Program Optimization
(Advisors: Hack, Smolka)
Tobias Tebbi, 2013,
won
Günther-Hotz-Medaille and Preis der Kühborth-Stiftung,
Unification Modulo Non-nested Recursion Schemes via Anchored Semi-Unification
(Advisor:Smolka)
Jonas Kaiser, 2012,
Formal Construction of a Set Theory in Coq
(Advisor: Brown)
Julian Backes, 2010,
Tableaux for Higher-Order Logic with If-Then-Else, Descriptions and Choice
(Advisor: Brown)
Christian Doczkal, 2009,
Formalizing TT-lifting in Isabelle/HOL-Nominal
(Advisor: Schwinghammer)
Daniel Götzmann, 2009,
A Tableau Prover for Hybrid Logic
(Advisor: Kaminski)
Niko Paltzer, 2007,
Infrastructure and Tools for Debugging Constraint Propagation
(Advisor: Tack)
Cătălin Hriţcu, 2007,
won
Günther-Hotz-Medaille,
Step-indexed Semantic Model of Types for the Functional Object Calculus
(Advisor: Schwinghammer)
Patrick Pekczynski,
2007,
Domain approximations for finite set constraint variables:
An integrated approach
(Advisor: Tack)
Mark Kaminski, 2006,
won
Günther-Hotz-Medaille and Preis der Kühborth-Stiftung,
Completeness Results for Higher-Order Logic
(Advisor: Smolka)
Murat Baktiev, 2006,
Permutation Semantics of Separation Logic
(Advisor: Schwinghammer)
Matthias Horbach,
2006,
Cut Elimination via Splitting versus Cut Elimination via Proof Nets
(Advisor: Straßburger)
Robert Grabowski,
2006,
Computational Aspects of Non-Projective Dependency Grammars
(Advisor: Kuhlmann)
Christian Müller,
2006,
Run-time Byte Code Compilation,
Optimization and Interpretation for Alice
(Advisor: Tack)
Mathias Möhl,
2006,
Drawings as Models of Syntactic Structure: Theory and Algorithms
(Advisor: Kuhlmann)
Patrick Cernko,
2004,
Realisierung einer Java Virtual Machine mit SEAM
(Advisor: Brunklaus)
Guido Tack,
2003,
won
Günther-Hotz-Medaille and VDI-Preis,
Transformation, Linearization and Minimization
of Data Graphs with Transients
(Advisors: Smolka,
Kornstaedt)
Dag Kröper,
2002,
Konzeption und Realisierung eines Bibliotheksverwaltungssystems
(Advisors: Schulte,
Smolka)
Martin Homik,
2002,
Ressourcenoptimierung eines Workflowproblems
(Advisors: Schulte,
Müller)
Jan Schwinghammer,
2002,
won
Günther-Hotz-Medaille,
A Concurrent Lambda-Calculus with Promises and Futures
(Advisors: Niehren, Smolka)
Ralph Debusmann,
2001,
A Declarative Grammar Formalism For Dependency Grammar
(Advisor: Duchier)
Manuel Bodirsky,
2001,
won
Günther-Hotz-Medaille,
Beta Reduction Constraints
(Advisor: Niehren),
Gerhard Schneider,
2000,
ML mit Typklassen
(Advisors: Rossberg,
Kornstaedt)
Thorsten Brunklaus,
2000,
Der Oz Inspector - Browsen: Interaktiver, einfacher, effizienter
(Advisor: Schulte)
Tim Priesnitz,
2000,
Entailment von nicht-strukturellen Teiltyp-Constraints
(Advisor: Niehren)
Daniel Simon,
1999,
An Implementation of the Programming Language DML in Java: Runtime Environment
(Advisor: Kornstaedt)
Andy Walter,
1999,
An Implementation of the Programming Language DML in Java: Compiler
(Advisor: Kornstaedt)
Alexander Koller,
1999,
Constraint Languages for Semantic Underspecification
(Advisor: Niehren)
Benjamin Lorenz,
1998,
Ein Debugger für Oz
(Advisors: Kornstaedt,
Scheidhauer)
Leif Kornstaedt, 1996,
Definition und Implementierung eines
Front-End-Generators für Oz
(Advisor: Schulte)
Kai Ibach, 1995,
OzFun: Eine funktionale Sprache für
gemischte Eager- und Lazy-Programmierung
(Advisor: Niehren)
Frank Zenner, 1995,
Anbindung einer grafischen Benutzerschnittstelle an Oz
(Advisors: Mehl, Scheidhauer)
Bernhard Latz, 1994,
Eine interaktive Benutzerschnittstelle für Oz
(Advisor: Smolka)
Stefan Jacobs, 1993,
Über Negation im logischen Programieren
(Advisor: Smolka)
Markus Höhfeld, 1988,
Ein Schema für constraint-basierte relationale Wissensbasen
(Advisor: Smolka, Uni KL)
Michael Schmitt, 1987,
Implementierung einer typisierten logischen Programmiersprache mit Gleichheit
(Advisor: Smolka, Uni KL)