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

\(\mathrm{HA}^{\omega }\)constructive mathematicsfan functionalGödel's system Tintuitionistic type theorysheavestopological modelstopos theoryuniform continuity

Mathematics Subject Classification ID

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

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

(15)

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

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)