Henning Basold


On this page, I collect code and references to code that belongs to publications or is otherwise interesting. My Github repository can be found here.

Code for paper "Type Theory based on Dependent Inductive and Coinductive Types"

Proof checker for the recursive logic presented in Section 5.2 of my thesis

The code can be found on github. Note that the implementation is not yet complete and has some problems. However, it works correctly for the examples provided in my thesis.

Correctness of μ-recursion Implemented Through Coinduction

Transitivity of the Substream Relation