Normalization for Type Theory with an Impredicative Universe
Ladda ner
Typ
Examensarbete för masterexamen
Master's Thesis
Master's Thesis
Program
Computer science – algorithms, languages and logic (MPALG), MSc
Publicerad
2024
Författare
Xie, Zongpu
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