Thesis
Computing spaces in type theory
- Abstract:
-
In this thesis, we develop multiple case studies computing with and in cubical type theory.
We begin by setting up a framework to compute with sets in the theorem prover Cubical Agda. Using the example of the powerset, we show how both mathematical definitions and programs can be expressed and related with one another in type theory. We show how a functional program implementing the powerset can be shown to satisfy the mathematical definition of the powerset, th...
Expand abstract
Actions
Access Document
- Files:
-
-
(Preview, Dissemination version, pdf, 625.1KB, Terms of use)
-
Authors
Contributors
+ Abramsky, S
- Institution:
- University of Oxford
- Division:
- MPLS
- Department:
- Computer Science
- Role:
- Supervisor
- ORCID:
- 0000-0003-3921-6637
+ Staton, S
- Institution:
- University of Oxford
- Division:
- MPLS
- Department:
- Computer Science
- Role:
- Supervisor
+ Gibbons, J
- Institution:
- University of Oxford
- Division:
- MPLS
- Department:
- Computer Science
- Role:
- Examiner
- ORCID:
- 0000-0002-8426-9917
+ Altenkirch, T
- Role:
- Examiner
+ Engineering and Physical Sciences Research Council
More from this funder
- Funder identifier:
- https://ror.org/0439y7842
- Funding agency for:
- Doré, M
- Grant:
- 2218874
- Programme:
- Studentship
+ University of Oxford
More from this funder
- Funder identifier:
- https://ror.org/052gg0110
- Funding agency for:
- Doré, M
- Programme:
- Scatcherd European Scholarship
- DOI:
- Type of award:
- DPhil
- Level of award:
- Doctoral
- Awarding institution:
- University of Oxford
- Language:
-
English
- Subjects:
- Deposit date:
-
2024-09-10
- ARK identifier:
Terms of use
- Copyright holder:
- Doré, M
- Copyright date:
- 2023
If you are the owner of this record, you can report an update to it here: Report update to this record