If you are interested in a topic for an RI Lab, please contact Prof. Smolka or a researcher of the Lab whose work you find interesting.
Format of Research Immersion Labs specified by the Graduate School.
Sergei Bozhko, 2020,
Mechanisation of Conditional Lower Bounds within P in Coq
(Advisor: Kunze)
Felix Rech, 2018,
Indexed Containers in UniMath
(Advisor: Schäfer)
Fabian Kunze, 2016
The Invariance Thesis for a Lambda Calculus:
Towards Formal Complexity Theory
(Advisor: Smolka)
Moritz Lichter, 2016
Büchi Automata in Coq
(Advisor: Smolka)
Kathrin Stark, 2016
Theory of Finitary Sets
(Advisor: Smolka)
Marc Roth, 2015
A Reasonable Time Measure for Weak Call-by-value Lambda Calculus
(Advisor: Smolka)
Hai Dang, 2015
Propositional Logic Revisited
(Advisor: Smolka)
Yannick Forster, 2015
Verified Extraction from Coq to a Lambda Calculus
(Advisor: Smolka)
Dominik Kirst, 2015
Inductive Characterization of Cumulative Hierarchy in ZF
(Advisor: Smolka)
Jonas Oberhauser, 2014
Termination with Intersection Types
(Advisor: Schäfer)
Marco Voigt, 2013,
Hilbert proof systems with proof terms and proof normalization
(Advisor: Smolka)
Gilles Nies, 2012,
Decidability and Completeness of Intuitionistic Propositional Logic
in Coq
(Advisors: Smolka and Brown)
Johannes Doerfert, Sebastian Hahn, Carsten Hornung, Steven Schäfer,
Bernhard Schommer, Tobias Tebbi, Andreas Teucke, 2012,
Compiler Verification in Coq
(Advisors:
Hack,
Schneider,
Smolka)