Normalization for Type Theory with an Impredicative Universe
| dc.contributor.author | Xie, Zongpu | |
| dc.contributor.department | Chalmers tekniska högskola / Institutionen för data och informationsteknik | sv |
| dc.contributor.department | Chalmers University of Technology / Department of Computer Science and Engineering | en |
| dc.contributor.examiner | Abel, Andreas | |
| dc.contributor.supervisor | Coquand, Thierry | |
| dc.date.accessioned | 2024-10-16T13:38:32Z | |
| dc.date.available | 2024-10-16T13:38:32Z | |
| dc.date.issued | 2024 | |
| dc.date.submitted | ||
| dc.description.abstract | 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. | |
| dc.identifier.coursecode | DATX05 | |
| dc.identifier.uri | http://hdl.handle.net/20.500.12380/308919 | |
| dc.language.iso | eng | |
| dc.setspec.uppsok | Technology | |
| dc.subject | Type theory | |
| dc.subject | Normalization | |
| dc.subject | Impredicativity | |
| dc.title | Normalization for Type Theory with an Impredicative Universe | |
| dc.type.degree | Examensarbete för masterexamen | sv |
| dc.type.degree | Master's Thesis | en |
| dc.type.uppsok | H | |
| local.programme | Computer science – algorithms, languages and logic (MPALG), MSc |