Explicit convertibility proofs in Pure Type Systems

Abstract

Most systems in Type Theory follow the Poincaré principle, which means that computations need no proof. This has disadvantages for long and complicated computations. We will introduce a new version of Type Theory where computations also require proof. In this new system the derivation of a judgement will be isomorphic to the term typed in the judgement. In the thesis we have proved that the new version is equivalent to the standard version. Type theory has applications in proof assistants, computer programmes which help checking a proof. To illustrate this use, the complete proof of this equivalence has been formalised in the proof assistant Coq.