Publications

Papers

Presentations

Formalizations

  • “Constructing the Propositional Truncation using Non-recursive HITs”. arXiv, code
    Floris van Doorn. Certified Proofs and Programs (CPP), 2016

  • “The Cayley-Dickson Construction in Homotopy Type Theory”. arXiv
    Ulrik Buchholtz and Egbert Rijke

Theses

  • Formalization of non-abelian topology for homotopy type theory. PDF, code
    Jakob von Raumer, MS thesis, Karlruhe Institute of Technology, 2015.

  • Simple Verification of Rust Programs via Functional Purification. PDF, code
    Sebastian Ullrich, MS thesis, Karlruhe Institute of Technology, 2016.

Courses

  • Logic and Proof. An introductory course for undergraduates. online tutorial, pdf
    Jeremy Avigad, Robert Y. Lewis, and Floris van Doorn.