Per Nilsson: Some simple proofs related to the Univalence Axiom formalized in Dedukti

abstract: Logical Frameworks (LF) have a long history going back to the Automath project. In this thesis an LF called Dedukti is used to im-plement some simple proofs related to the Univalence Axiom (UA). One key feature of Dedukti is that rewrite rules as well as β-reduction is used when types are checked. The thesis explains some of the the-oretical foundations of Dedukti. It also exemplifies how to express propositions as types and proofs as terms with corresponding type. It covers some aspects of term rewriting, typed λ-calculus, Pure Type Systems (PTS) and it shows how two different variants of universe hierarchies can be embedded in Dedukti.