Finiteness in cubical type theory

dc.availability.bitstreamopenaccess
dc.contributor.advisorProvan, Gregoryen
dc.contributor.advisorexternalWu, Nicolasen
dc.contributor.authorKidney, Donnacha Oisín
dc.contributor.funderScience Foundation Irelanden
dc.date.accessioned2021-05-18T09:03:41Z
dc.date.available2021-05-18T09:03:41Z
dc.date.issued2020-09
dc.date.submitted2020-09
dc.description.abstractThis thesis will explore and explain finiteness in constructive mathematics: using this setting, it will also serve as an introduction to constructive mathematics in Cubical Agda, and some related topics.en
dc.description.statusNot peer revieweden
dc.description.versionAccepted Versionen
dc.format.mimetypeapplication/pdfen
dc.identifier.citationKidney, D. O. 2020. Finiteness in cubical type theory MRes Thesis, University College Cork.en
dc.identifier.endpage84en
dc.identifier.urihttps://hdl.handle.net/10468/11338
dc.language.isoenen
dc.publisherUniversity College Corken
dc.relation.projectinfo:eu-repo/grantAgreement/SFI/SFI Research Centres/13/RC/2094/IE/Lero - the Irish Software Research Centre/en
dc.rights© 2020, Donnacha Oisín Kidney.en
dc.rights.urihttps://creativecommons.org/licenses/by-sa/4.0/en
dc.subjectAgdaen
dc.subjectHaskellen
dc.subjectHomotopy type theoryen
dc.subjectAutomated proof assistantsen
dc.subjectCubical type theoryen
dc.subjectDependent typeen
dc.subjectConstructive mathematicsen
dc.subjectTopos theoryen
dc.subjectAutomated theorem provingen
dc.titleFiniteness in cubical type theoryen
dc.typeMasters thesis (Research)en
dc.type.qualificationlevelMastersen
dc.type.qualificationnameMSc - Master of Scienceen
Files
Original bundle
Now showing 1 - 2 of 2
Loading...
Thumbnail Image
Name:
masters-thesis.pdf
Size:
764.17 KB
Format:
Adobe Portable Document Format
Description:
Full Text E-thesis
Loading...
Thumbnail Image
Name:
3. Donncha Oisin Kidney Submission for Exam Form Oisin Kidney 28082020 GP - Donnacha Oisin Kidney.pdf
Size:
394.13 KB
Format:
Adobe Portable Document Format
Description:
Submission for Examination Form
License bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
license.txt
Size:
5.2 KB
Format:
Item-specific license agreed upon to submission
Description: