A Logical Relation for Dependent Type Theory Formalized in Agda

dc.contributor.author	Öhman, Joakim
dc.date.accessioned	2017-02-27T10:13:31Z
dc.date.available	2017-02-27T10:13:31Z
dc.date.issued	2017-02-27
dc.identifier.uri	http://hdl.handle.net/2077/51820
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.language.iso	eng	sv
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.setspec.uppsok	Technology
dc.type.uppsok	H2
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.type.degree	Student essay