# Research Immersion Labs, Programming Systems Lab, Prof. Gert Smolka

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.

## Research Immersion Labs in Progress

## Research Immersion Labs Completed

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)

Legal notice, Privacy policy