A constructive model of uniform continuity

DOI10.1007/978-3-642-38946-7_18MaRDI QIDQ5300905zbMATH OpenOpenAlexFDO

Authors Chuangjie Xu, Martín Escardo

Publication date 28 June 2013

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-38946-7_18

zbMATH Keywords

constructive mathematicsuniform continuitysheavesfan functionalintuitionistic type theorytopological modelstopos theoryGödel's system T\(\mathrm{HA}^{\omega }\)

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Other constructive mathematics (03F65) Categorical logic, topoi (03G30) Presheaves and sheaves in general topology (54B40) Type theory (03B38)

Recommendations

• A constructive manifestation of the Kleene-Kreisel continuous functionals
• Continuity of Gödel's system T definable functionals via effectful forcing
• The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation
• Decidable fan theorem and uniform continuity theorem with continuous moduli
• A note on forcing and type theory

Cited in

(13)

• Continuous and monotone machines
• Gardening with the pythia a model of continuity in a dependent setting
• A Computable Solution to Partee’s Temperature Puzzle
• A constructive manifestation of the Kleene-Kreisel continuous functionals
• Continuity of Gödel's system T definable functionals via effectful forcing
• The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation
• \(\text{TT}^\Box_{\mathcal{C}}\): a family of extensional type theories with effectful realizers of continuity
• A note on forcing and type theory
• Compactly generated spaces and quasi-spaces in topology
• A computational interpretation of forcing in type theory
• Coherence spaces and uniform continuity
• Validating Brouwer's continuity principle for numbers using named exceptions
• Synthesis of moduli of uniform continuity by the monotone Dialectica interpretation in the proof-system \texttt{MinLog}

Describes a project that uses

Uses Software

• Agda

This page was built for publication: A constructive model of uniform continuity

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5300905)