A constructive manifestation of the Kleene-Kreisel continuous functionals

DOI10.1016/J.APAL.2016.04.011MaRDI QIDQ290639zbMATH OpenOpenAlexFDO

Authors Chuangjie Xu, Martín Escardo

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) Higher-type and set recursion theory (03D65) Nonclassical models (Boolean-valued, sheaf, etc.) (03C90)

Recommendations

• Stein's idea and minimax admissible estimation of a multivariate normal mean
• On homogeneous James-Stein type estimators
• Combining Minimax Shrinkage Estimators
• Minimax multiple shrinkage estimation
• Minimax shrinkage estimators and estimators dominating the James-Stein estimator under the balanced loss function

Cites work

• scientific article; zbMATH DE number 445156 (Why is no real title available?)
• scientific article; zbMATH DE number 3867322 (Why is no real title available?)
• scientific article; zbMATH DE number 3825806 (Why is no real title available?)
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 3918365 (Why is no real title available?)
• scientific article; zbMATH DE number 4070894 (Why is no real title available?)
• scientific article; zbMATH DE number 193320 (Why is no real title available?)
• scientific article; zbMATH DE number 2079044 (Why is no real title available?)
• scientific article; zbMATH DE number 1840601 (Why is no real title available?)
• scientific article; zbMATH DE number 2204752 (Why is no real title available?)
• scientific article; zbMATH DE number 3310901 (Why is no real title available?)
• A computational interpretation of forcing in type theory
• A constructive model of uniform continuity
• A note on forcing and type theory
• Compactly generated domain theory
• Comparing Cartesian closed categories of (core) compactly generated spaces
• Computing with Functionals—Computability Theory or Computer Science?
• Continuous truth. II: Reflections
• Convenient categories of smooth spaces
• Dependent Types at Work
• Dependently typed programming in Agda
• Equilogical spaces
• Filter spaces and continuous functionals
• Higher-order computability
• Homotopy type theory. Univalent foundations of mathematics
• Internal type theory
• Locally cartesian closed categories and type theory
• On a Topological Topos
• On the ubiquity of certain total type structures
• Quasi-topologies
• Recursion on the countable functionals
• Revisiting the categorical interpretation of dependent type theory
• Sheaf models for choice sequences
• Sheaves in geometry and logic: a first introduction to topos theory
• The biequivalence of locally Cartesian closed categories and Martin-Löf type theories
• The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation

Cited in

(11)

• A Computable Solution to Partee’s Temperature Puzzle
• scientific article; zbMATH DE number 4114613 (Why is no real title available?)
• Computable analysis and notions of continuity in \textsc{Coq}
• scientific article; zbMATH DE number 7199581 (Why is no real title available?)
• Closed subsets in Bishop topological groups
• A constructive model of uniform continuity
• scientific article; zbMATH DE number 495568 (Why is no real title available?)
• Concrete categories and higher-order recursion. With applications including probability, differentiability, and full abstraction
• Synthetic topology in Homotopy Type Theory for probabilistic programming
• Quantitative continuity and Computable Analysis in Coq
• Gardening with the pythia a model of continuity in a dependent setting

Describes a project that uses

Uses Software

• Agda

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

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