A constructive model of uniform continuity

Chuangjie Xu, Martín Escardó

Research output: Chapter in Book/Report/Conference proceedingConference contribution

10 Citations (Scopus)

Abstract

We construct a continuous model of Gödel's system T and its logic HAω in which all functions from the Cantor space 2 to the natural numbers are uniformly continuous. Our development is constructive, and has been carried out in intensional type theory in Agda notation, so that, in particular, we can compute moduli of uniform continuity of T-definable functions 2 → ℕ. Moreover, the model has a continuous Fan functional of type (2 → ℕ) → ℕ that calculates moduli of uniform continuity. We work with sheaves, and with a full subcategory of concrete sheaves that can be presented as sets with structure, which can be regarded as spaces, and whose natural transformations can be regarded as continuous maps.

Original languageEnglish
Title of host publicationTyped Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings
Pages236-349
Number of pages114
DOIs
Publication statusPublished - 2013
Event11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013 - Eindhoven, Netherlands
Duration: 26 Jun 201328 Jun 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7941 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013
Country/TerritoryNetherlands
CityEindhoven
Period26/06/1328/06/13

Keywords

  • Constructive mathematics
  • Fan functional
  • Gödel's system T
  • HA
  • intuitionistic type theory
  • sheaves
  • topological models
  • topos theory
  • uniform continuity

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'A constructive model of uniform continuity'. Together they form a unique fingerprint.

Cite this