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

Saarland University Computer Science

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