| dc.contributor.author | Kløvstad, Åsmund Aqissiaq Arild | |
| dc.date.accessioned | 2022-06-28T00:00:53Z | |
| dc.date.available | 2022-06-28T00:00:53Z | |
| dc.date.issued | 2022-06-01 | |
| dc.date.submitted | 2022-06-27T22:02:31Z | |
| dc.identifier.uri | https://hdl.handle.net/11250/3001129 | |
| dc.description.abstract | We consider theoretical models of version control systems based on Homotopy Type Theory (HoTT). The main contribution is an implementation of Angiuli et al.’s Homotopical Patch Theory in Cubical Agda. Additionally the first chapter contains an approachable introduction to HoTT and Cubical Agda aimed at an audience of interested computer science students covering dependent Martin-Löf-style type theory, propositions as types, univalent foundations, higher inductive types and CCHM cubical type theory. Finally, we discuss some other approaches to a theory of version control systems in Darcs’ “algebra of patches” and an unsuccessful attempt to model repositories in type theory as coequalizers. | |
| dc.language.iso | eng | |
| dc.publisher | The University of Bergen | |
| dc.rights | Copyright the Author. All rights reserved | |
| dc.subject | Version Control | |
| dc.subject | Cubical Agda | |
| dc.subject | Agda | |
| dc.subject | Cubical Type Theory | |
| dc.subject | Type Theory | |
| dc.subject | Homotopy Type Theory | |
| dc.title | A Cubical Implementation of Homotopical Patch Theory | |
| dc.type | Master thesis | |
| dc.date.updated | 2022-06-27T22:02:31Z | |
| dc.rights.holder | Copyright the Author. All rights reserved | |
| dc.description.degree | Master's Thesis in Informatics | |
| dc.description.localcode | INF399 | |
| dc.description.localcode | MAMN-INF | |
| dc.description.localcode | MAMN-PROG | |
| dc.subject.nus | 754199 | |
| fs.subjectcode | INF399 | |
| fs.unitcode | 12-12-0 | |
