A Logical Relation for Dependent Type Theory Formalized in Agda
| dc.contributor.author | Öhman, Joakim | |
| dc.contributor.department | Göteborgs universitet/Institutionen för data- och informationsteknik | swe |
| dc.contributor.department | University of Gothenburg/Department of Computer Science and Engineering | eng |
| dc.date.accessioned | 2017-02-27T10:13:31Z | |
| dc.date.available | 2017-02-27T10:13:31Z | |
| dc.date.issued | 2017-02-27 | |
| dc.description.abstract | When writing proofs, it is desirable to show that one’s proof is correct. With formalising a proof in dependent type theory, it is implied that the proof is correct as long as the type theory is correct. <br><br> This thesis covers the formalisation of a fragment of Martin-Löf type theory with one universe, for which its grammar and judgements are formalised. A logical relation is then defined as well as validity judgements and proven valid with respect to the type system. This is then used to prove canonicity and injectivity of the II -type. | sv |
| dc.identifier.uri | http://hdl.handle.net/2077/51820 | |
| dc.language.iso | eng | sv |
| dc.setspec.uppsok | Technology | |
| dc.subject | type theory | sv |
| dc.subject | dependent types | sv |
| dc.subject | logical relation | sv |
| dc.subject | Agda | sv |
| dc.subject | formalization | sv |
| dc.title | A Logical Relation for Dependent Type Theory Formalized in Agda | sv |
| dc.type | text | |
| dc.type.degree | Student essay | |
| dc.type.uppsok | H2 |