From sets and types to topology and analysis - Towards practicable foundations for constructive mathematics
From sets and types to topology and analysis - Towards practicable foundations for constructive mathematics
复制标题
从集合和类型到拓扑和分析 - 迈向构造性数学的实用基础
DOI：
10.1093/acprof:oso/9780198566519.001.0001
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
P. Schuster
中科院分区：
文献类型：
--
作者：
Laura Crosilla;P. Schuster
埃雷特·毕晓普构造集论中的广义归纳定义2。构造集理论及其范畴论模型构造集理论的预表模型Toposes中的宇宙构建数学的极简基础依赖类型论中的交互规划与弱终代数归纳定义和选择原则在程序综合中的应用经典的和构造的概念和证明的对偶性实线和形式空间的连续性构造拓扑中的分离属性空间是共子体。局部紧形拓扑在归纳生成拓扑上的预测幂。通往第谷诺夫14号的一些建设性道路。Krull维15的初等表征。构造逆数学：紧性用构造紧致逼近可积集构造数学中c*-代数理论的导论18。巴拿赫代数元素数值范围的近似。rn20上局部凸拓扑的构造唯一性。不可分Banach空间的可计算性与Landau定理
Introduction Errett Bishop 1. Generalized Inductive Definitions in Constructive Set Theory 2. Constructive Set Theories and their Category-theoretic Models 3. Presheaf models for Constructive Set Theories 4. Universes in Toposes 5. Toward a minimalistic foundation for constructive mathematics 6. Interactive Programs and Weakly Final Coalgebras in Dependent Type Theory 7. Applications of inductive definitions and choice principles to program synthesis 8. The duality of lcassical and constructive notions and proofs 9. Continuity on the real line and in formal spaces 10. Separation Properties in Constructive Topology 11. Spaces as comonoids 12. Predicative exponentiation of locally compact formal topologies over inductively generated ones 13. Some constructive roads to Tychonoff 14. An elementary characterisation of Krull dimension 15. Constructive reverse mathematics: compactness properties 16. Approximating integrable sets by compacts constructively 17. An introduction to the theory of c*-algegras in constructive mathematics 18. Approximations to the numerical range of an element of a Banach algebra 19. The constructive uniqueness of the locally convex topology on rn 20. Computability on Non-Separable Banach Spaces and Landau's Theorem