A constructive manifestation of the Kleene-Kreisel continuous functionals

DOI10.1016/j.apal.2016.04.011zbMath1402.03020OpenAlexW2341132922MaRDI QIDQ290639

Chuangjie Xu, Martín Hötzel Escardó

Publication date: 3 June 2016

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2016.04.011

zbMATH Keywords

constructive mathematicsuniform continuitysheavesfan functionalintuitionistic type theoryKleene-Kreisel continuous functionals

Mathematics Subject Classification ID

Metamathematics of constructive systems (03F50) Nonclassical models (Boolean-valued, sheaf, etc.) (03C90) Higher-type and set recursion theory (03D65)

Related Items (6)

Synthetic topology in Homotopy Type Theory for probabilistic programming ⋮ Unnamed Item ⋮ A Computable Solution to Partee’s Temperature Puzzle ⋮ Quantitative continuity and Computable Analysis in Coq ⋮ Unnamed Item ⋮ Closed subsets in Bishop topological groups

Uses Software

• Agda

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Sheaf models for choice sequences
• Recursion on the countable functionals
• Sheaves in geometry and logic: a first introduction to topos theory
• Equilogical spaces
• Comparing Cartesian closed categories of (core) compactly generated spaces
• Revisiting the categorical interpretation of dependent type theory
• Quasi-topologies
• Continuous Truth II: Reflections
• The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories
• Filter spaces and continuous functionals
• A Note on Forcing and Type Theory
• Convenient categories of smooth spaces
• Locally cartesian closed categories and type theory
• Higher-Order Computability
• Dependently Typed Programming in Agda
• On a Topological Topos
• Internal type theory
• Dependent Types at Work
• A Computational Interpretation of Forcing in Type Theory
• The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation
• A Constructive Model of Uniform Continuity
• Homotopy Type Theory: Univalent Foundations of Mathematics
• On the ubiquity of certain total type structures
• Computing with Functionals—Computability Theory or Computer Science?
• Compactly generated domain theory

This page was built for publication: A constructive manifestation of the Kleene-Kreisel continuous functionals