Research Projects

The Master of Logic allows students to earn up to 24 EC via research projects. These are the research projects I have worked on so far.

Formal Analysis of Material Dialogues for FOL

This project was supervised by Dominik Kirst from Saarland University. It can be viewed as me carrying out one of the ideas mentioned in the “future work” section of my Bachelor’s thesis. Dialogical logic, originally put forward by Paul Lorenzen, captures the notion of first-order validity in terms of games modeled after a debate. Material dialogues, the variant we examine in this project, has a distinctly model-theoretic flavor compared to the formal dialogues usually considered in the literature. Arguably, it also is closer to Lorenzen’s original formulation of dialogical logic.

In the course of the project, I gave a novel formalization of material dialogues, using insights from my Bachelor’s thesis. I examined the thereby arising semantics for first-order logic in the calculus of inductive constructions, with special attention paid to the constructivity of completeness proofs with regards to them. I obtained the following results:

We are currently in the process of turning the project’s results into a paper which we hope to present at a conference.


Aczel’s Type-Theoretic Interpretation of CZF

This project was supervised by Robert Passmann. It can be viewed as a culmination of the set theory lectures which I took during the Master of Logic and my background in type theory. I read Peter Aczel’s three seminal papers on his interpretation of constructive Zeremelo-Fraenkel set theory into Martin Löf’s dependent type theory and summarized them in a manner accessible to anyone with a little knowledge about axiomatic set theory and no background in type theory.

The summary was published as part of the ILLC technical report series. I also gave a talk on the subject at the Mathematische Logik research seminar at Hamburg university on the 21. January 2021.


Categorical Normalization by Evaluation

This project was supervised by Benno van den Berg. We read papers on normalization by evaluation, a semantic technique for normalizing the terms of a type theory. The focus was on papers which made use of categorical semantics (see the references below). To close the project, I combined the insights gleamed from the reading to try to transfer a technique for handling certain additional constants, introduced in the seminal paper on NBE by Berger and Schwichtenberg, to the categorical setting of the reduction free normalization proof of Altenkirch et. al. I succeeded in adapting the categorical normalization interpretation from Altenkirch et. al. to admit Schwichtenberg’s and Berger’s inductive correctness proof of the normalization theorem with the added constants. However, I did not manage to extend the categorical proof of the normalization theorem, given by Altenkirch et. al., to cover generic constants with similar conditions.