Types with extra structure: predicates, equations, composition
Intuitionistic type theory was first introduced by Martin-Lof [1984] as a foundation for constructive mathematics and also serves as a dependently typed programming language. Dependent types provide us with a framework to reason about and guide the construction of programs by specifying both their s...
| Main Author: | |
|---|---|
| Format: | Thesis (University of Nottingham only) |
| Language: | English |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://eprints.nottingham.ac.uk/79401/ |