Canonicity of the Mahlo Universe
| dc.contributor.author | Kubánek, Ondrej | |
| 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 | Coquand, Thierry | |
| dc.contributor.supervisor | Kovacs, Andras | |
| dc.date.accessioned | 2025-11-19T07:36:34Z | |
| dc.date.issued | 2025 | |
| dc.date.submitted | ||
| dc.description.abstract | The thesis presents a proof of canonicity of the external Mahlo universe using the gluing technique. The used metatheory is an extensional type theory extended with indexed induction-recursion to express the reducibility predicate for the external Mahlo universe. This is motivated by the fact that the Mahlo universe can express certain inductive-recursive definitions and so understanding the metatheory for the external Mahlo universe should help with metatheory for induction-recursion. | |
| dc.identifier.coursecode | DATX05 | |
| dc.identifier.uri | http://hdl.handle.net/20.500.12380/310758 | |
| dc.language.iso | eng | |
| dc.relation.ispartofseries | CSE 25-64 | |
| dc.setspec.uppsok | Technology | |
| dc.subject | type theory, metatheory, gluing, canonicity, mahlo universe, inductionrecursion | |
| dc.title | Canonicity of the Mahlo 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 |