Type checking and normalisation
This thesis is about Martin-Löf's intuitionistic theory of types (type theory). Type theory is at the same time a formal system for mathematical proof and a dependently typed programming language. Dependent types are types which depend on data and therefore to type check dependently typed progr...
| Main Author: | |
|---|---|
| Format: | Thesis (University of Nottingham only) |
| Language: | English |
| Published: |
2009
|
| Online Access: | https://eprints.nottingham.ac.uk/10824/ |