Finiteness in cubical type theory
dc.availability.bitstream | openaccess | |
dc.contributor.advisor | Provan, Gregory | en |
dc.contributor.advisorexternal | Wu, Nicolas | en |
dc.contributor.author | Kidney, Donnacha Oisín | |
dc.contributor.funder | Science Foundation Ireland | en |
dc.date.accessioned | 2021-05-18T09:03:41Z | |
dc.date.available | 2021-05-18T09:03:41Z | |
dc.date.issued | 2020-09 | |
dc.date.submitted | 2020-09 | |
dc.description.abstract | This 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.status | Not peer reviewed | en |
dc.description.version | Accepted Version | en |
dc.format.mimetype | application/pdf | en |
dc.identifier.citation | Kidney, D. O. 2020. Finiteness in cubical type theory MRes Thesis, University College Cork. | en |
dc.identifier.endpage | 84 | en |
dc.identifier.uri | https://hdl.handle.net/10468/11338 | |
dc.language.iso | en | en |
dc.publisher | University College Cork | en |
dc.relation.project | info: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.uri | https://creativecommons.org/licenses/by-sa/4.0/ | en |
dc.subject | Agda | en |
dc.subject | Haskell | en |
dc.subject | Homotopy type theory | en |
dc.subject | Automated proof assistants | en |
dc.subject | Cubical type theory | en |
dc.subject | Dependent type | en |
dc.subject | Constructive mathematics | en |
dc.subject | Topos theory | en |
dc.subject | Automated theorem proving | en |
dc.title | Finiteness in cubical type theory | en |
dc.type | Masters thesis (Research) | en |
dc.type.qualificationlevel | Masters | en |
dc.type.qualificationname | MSc - Master of Science | en |
Files
Original bundle
1 - 2 of 2
Loading...
- Name:
- masters-thesis.pdf
- Size:
- 764.17 KB
- Format:
- Adobe Portable Document Format
- Description:
- Full Text E-thesis
Loading...
- 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
1 - 1 of 1
Loading...
- Name:
- license.txt
- Size:
- 5.2 KB
- Format:
- Item-specific license agreed upon to submission
- Description: