Code
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
- Definition of the substream relation
- Definition of Stream Selectors
- Definition of the selector-based substream relation
- Composition of stream selectors
- Proof that composing selectors is the same as composing selection functions
- Proof that the selector-based substream relation is transitive
- Proof that the selector-based substream relation and the direct definition are equivalent
- Proof that the substream relation is transitive