Hittauppsatser.se

Uppsats

Normalization for Type Theory with an Impredicative Universe

H

Xie, Zongpu

Chalmers tekniska högskola / Institutionen för data och informationsteknik

Publicerad: 2024

Språk: Engelska

Nyckelord

klicka för att söka
⌕Normalization⌕Type theory⌕Impredicativity

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.

Information

Författare
Xie, Zongpu
Lärosäte / institution
Chalmers tekniska högskola / Institutionen för data och informationsteknik
Publiceringsdatum
2024
Uppsatstyp
H
Språk
Engelska
Nyckelord
⌕Normalization⌕Type theory⌕Impredicativity

Utforska vidare

Liknande uppsatser

Uppsatser med liknande ämnen och nyckelord.