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/ |
| _version_ | 1848791136363085824 |
|---|---|
| author | Chapman, James Maitland |
| author_facet | Chapman, James Maitland |
| author_sort | Chapman, James Maitland |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | 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 programming we need to perform computation(normalisation) in types.
Implementations of type theory (usually some kind of automatic theorem prover or interpreter) have at their heart a type checker. Implementations of type checkers for type theory have at their heart a normaliser. In this thesis I consider type checking as it might form the basis of an implementation of type theory in the functional language Haskell and then normalisation in the more rigorous setting of the dependently typed languages Epigram and Agda. I investigate a method of proving normalisation called Big-Step Normalisation (BSN). I apply BSN to a number of calculi of increasing sophistication and provide machine checked proofs of meta theoretic properties. |
| first_indexed | 2025-11-14T18:23:43Z |
| format | Thesis (University of Nottingham only) |
| id | nottingham-10824 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| language | English |
| last_indexed | 2025-11-14T18:23:43Z |
| publishDate | 2009 |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-108242025-02-28T11:09:50Z https://eprints.nottingham.ac.uk/10824/ Type checking and normalisation Chapman, James Maitland 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 programming we need to perform computation(normalisation) in types. Implementations of type theory (usually some kind of automatic theorem prover or interpreter) have at their heart a type checker. Implementations of type checkers for type theory have at their heart a normaliser. In this thesis I consider type checking as it might form the basis of an implementation of type theory in the functional language Haskell and then normalisation in the more rigorous setting of the dependently typed languages Epigram and Agda. I investigate a method of proving normalisation called Big-Step Normalisation (BSN). I apply BSN to a number of calculi of increasing sophistication and provide machine checked proofs of meta theoretic properties. 2009-07-23 Thesis (University of Nottingham only) NonPeerReviewed application/pdf en arr https://eprints.nottingham.ac.uk/10824/1/thesis.pdf Chapman, James Maitland (2009) Type checking and normalisation. PhD thesis, University of Nottingham. |
| spellingShingle | Chapman, James Maitland Type checking and normalisation |
| title | Type checking and normalisation |
| title_full | Type checking and normalisation |
| title_fullStr | Type checking and normalisation |
| title_full_unstemmed | Type checking and normalisation |
| title_short | Type checking and normalisation |
| title_sort | type checking and normalisation |
| url | https://eprints.nottingham.ac.uk/10824/ |