Bootstrapping extensionality: Agda formalization
| dc.contributor.author | Sestini, Filippo | |
| dc.date.accessioned | 2023-03-27T12:12:47Z | |
| dc.date.available | 2023-03-27T12:12:47Z | |
| dc.date.issued | 2023-03-27 | |
| dc.identifier.uri | https://rdmc.nottingham.ac.uk/handle/internal/10461 | |
| dc.description.abstract | Agda formalization covering the mathematical content of the PhD thesis "Bootstrapping Extensionality". | en_UK |
| dc.language.iso | en | en_UK |
| dc.publisher | The University of Nottingham | en_UK |
| dc.rights | CC-BY | * |
| dc.rights.uri | https://creativecommons.org/licenses/by/4.0/ | * |
| dc.subject.lcsh | Type theory | en_UK |
| dc.title | Bootstrapping extensionality: Agda formalization | en_UK |
| dc.type | dataset | |
| dc.identifier.doi | http://doi.org/10.17639/nott.7291 | |
| dc.subject.free | type theory, agda, iits, extensionality, setoids | en_UK |
| dc.subject.jacs | Mathematical Sciences::Mathematics | en_UK |
| dc.subject.lc | Q Science::QA Mathematics | en_UK |
| uon.division | University of Nottingham, UK Campus::Faculty of Science::School of Computer Science | en_UK |
| uon.funder.controlled | Other | en_UK |
| uon.datatype | Source code | en_UK |
| uon.collectionmethod | Code editor | en_UK |
Files in this item
This item appears in the following Collection(s)
-
Public Research Data
A collection of research data, held in this repository, that is publicly available, except where individual embargoes apply
Except where otherwise noted, this item's license is described as Creative Commons by Attribution