Higher inductive types, inductive families, and inductive-inductive types
Martin-Löf type theory is a formal language which is used both as a foundation for mathematics and the theoretical basis of a range of functional programming languages. Inductive types are an important part of type theory which is necessary to express data types by giving a list of rules stating how...
| Main Author: | |
|---|---|
| Format: | Thesis (University of Nottingham only) |
| Language: | English |
| Published: |
2020
|
| Subjects: | |
| Online Access: | https://eprints.nottingham.ac.uk/60036/ |