Normalization for Type Theory with an Impredicative Universe
Ladda ner
Publicerad
Författare
Typ
Examensarbete för masterexamen
Master's Thesis
Master's Thesis
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
This thesis presents a novel proof of canonicity and normalization for a type theory a proof relevant impredicative universe and a hierarchy of predicative universes. The proof uses Artin gluing, and is structured in a modular way that makes it easier to extend to new type formers.
Beskrivning
Ämne/nyckelord
Type theory, Normalization, Impredicativity