View Item 
        •   Utrecht University Student Theses Repository Home
        • UU Theses Repository
        • Theses
        • View Item
        •   Utrecht University Student Theses Repository Home
        • UU Theses Repository
        • Theses
        • View Item
        JavaScript is disabled for your browser. Some features of this site may not work without it.

        Browse

        All of UU Student Theses RepositoryBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects

        Explicit convertibility proofs in Pure Type Systems

        Thumbnail
        View/Open
        thesis.pdf (767.7Kb)
        Publication date
        2013
        Author
        Doorn, F.P. van
        Metadata
        Show full item record
        Summary
        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.
        URI
        https://studenttheses.uu.nl/handle/20.500.12932/13854
        Collections
        • Theses
        Utrecht university logo