A constructive manifestation of the Kleene-Kreisel continuous functionals

DOI10.1016/J.APAL.2016.04.011zbMATH Open1402.03020OpenAlexW2341132922MaRDI QIDQ290639FDOQ290639

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

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

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)

Cites Work

• Dependently typed programming in Agda
• Convenient categories of smooth spaces
• Sheaves in geometry and logic: a first introduction to topos theory
• A note on forcing and type theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Dependent Types at Work
• A computational interpretation of forcing in type theory
• Title not available (Why is that?)
• Homotopy type theory. Univalent foundations of mathematics
• Recursion on the countable functionals
• 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
• Title not available (Why is that?)
• Locally cartesian closed categories and type theory
• Title not available (Why is that?)
• Higher-order computability
• Title not available (Why is that?)
• On a Topological Topos
• Internal type theory
• The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation
• A constructive model of uniform continuity
• Title not available (Why is that?)
• On the ubiquity of certain total type structures
• Computing with Functionals—Computability Theory or Computer Science?
• Compactly generated domain theory
• Title not available (Why is that?)
• Sheaf models for choice sequences

Cited In (11)

• Synthetic topology in Homotopy Type Theory for probabilistic programming
• Title not available (Why is that?)
• Gardening with the pythia a model of continuity in a dependent setting
• A Computable Solution to Partee’s Temperature Puzzle
• A constructive model of uniform continuity
• Quantitative continuity and Computable Analysis in Coq
• Concrete categories and higher-order recursion. With applications including probability, differentiability, and full abstraction
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Closed subsets in Bishop topological groups

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)