A continuous computational interpretation of type theories

Xu, Chuangjie (2015). A continuous computational interpretation of type theories. University of Birmingham. Ph.D.

[img]
Preview
Xu15PhD.pdf
PDF - Accepted Version

Download (1MB)

Abstract

This thesis provides a computational interpretation of type theory validating Brouwer’s uniform-continuity principle that all functions from the Cantor space to natural numbers are uniformly continuous, so that type-theoretic proofs with the principle as an assumption have computational content.
For this, we develop a variation of Johnstone’s topological topos, which consists of sheaves on a certain uniform-continuity site that is suitable for predicative, constructive reasoning. Our concrete sheaves can be described as sets equipped with a suitable continuity structure, which we call C-spaces, and their natural transformations can be regarded as continuous maps. The Kleene-Kreisel continuous functional can be calculated within the category of C-spaces.
Our C-spaces form a locally cartesian closed category with a natural numbers object, and hence give models of Gödel’s system T and of dependent type theory. Moreover, the category has a fan functional that continuously compute moduli of uniform continuity, which validates the uniform-continuity principle formulated as a skolemized formula in system T and as a type via the Curry-Howard interpretation in dependent type theory.
We emphasize that the construction of C-spaces and the verification of the uniform-continuity principles have been formalized in intensional Martin-Löf type theory in Agda notation.

Type of Work: Thesis (Doctorates > Ph.D.)
Award Type: Doctorates > Ph.D.
Supervisor(s):
Supervisor(s)EmailORCID
Escardo, MartinUNSPECIFIEDUNSPECIFIED
Licence:
College/Faculty: Colleges (2008 onwards) > College of Engineering & Physical Sciences
School or Department: School of Computer Science
Funders: Other
Other Funders: The University of Birmingham
Subjects: Q Science > QA Mathematics > QA75 Electronic computers. Computer science
URI: http://etheses.bham.ac.uk/id/eprint/5967

Actions

Request a Correction Request a Correction
View Item View Item

Downloads

Downloads per month over past year