Extensional constructive real analysis via locators

DOI10.1017/S0960129520000171MaRDI QIDQ5156769zbMATH OpenOpenAlexFDO

Authors Auke B. Booij

Publication date 11 October 2021

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1805.06781

zbMATH Keywords

constructive analysisconstructive mathematicsdependent type theoryexact real arithmetichomotopy type theory

Mathematics Subject Classification ID

Type theory (03B38) Constructive and recursive analysis (03F60)

Recommendations

• Generalized real numbers in constructive mathematics
• Constructive analysis, types and exact real numbers
• Implementing constructive real analysis (preliminary report)
• Representations of the real numbers and of the open subsets of the set of real numbers
• Constructive analysis with witnesses

Cites work

• A lambda calculus for real analysis
• Constructive analysis with witnesses
• Constructivism in mathematics. An introduction. Volume II
• Formally verified approximations of definite integrals
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 1665440 (Why is no real title available?)
• scientific article; zbMATH DE number 4002093 (Why is no real title available?)
• scientific article; zbMATH DE number 4070894 (Why is no real title available?)
• scientific article; zbMATH DE number 2152236 (Why is no real title available?)
• Notions of anonymous existence in Martin-Löf type theory
• On the Cauchy completeness of the constructive Cauchy reals
• Techniques of constructive analysis
• The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation
• The intermediate value theorem in constructive mathematics without choice

Cited in

(3)

• On the extended Hensel construction and its application to the computation of real limit points
• Constructive theory of the lower power locale
• The interval domain in homotopy type theory

Describes a project that uses

Uses Software

• HoTT
• Coq
• GitHub

This page was built for publication: Extensional constructive real analysis via locators

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