On the Constructive and Computational Content of Abstract Mathematics

DOI10.1007/978-3-030-20447-1_6zbMath1469.03169OpenAlexW2966999886MaRDI QIDQ3305627

No author found.

Publication date: 10 August 2020

Published in: Mathesis Universalis, Computability and Proof (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-20447-1_6

Mathematics Subject Classification ID

Constructive and recursive analysis (03F60) Axiom of choice and related propositions (03E25)

Uses Software

• Minlog

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A universal Krull-Lindenbaum theorem
• Proofs, programs, processes
• Proving open properties by induction
• Optimized program extraction for induction and coinduction
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• A Direct Proof of Wiener’s Theorem
• From coinductive proofs to exact real arithmetic: theory and applications
• Minlog - A Tool for Program Extraction Supporting Algebras and Coalgebras
• Proofs and Computations
• A logical approach to abstract algebra
• Axiom of Choice and Complementation
• Choice Implies Excluded Middle
• Continuous Lattices and Domains
• The axiom of choice and the law of excluded middle in weak set theories
• THE INDEPENDENCE OF THE CONTINUUM HYPOTHESIS
• Consistency of the Continuum Hypothesis. (AM-3)
• On the interpretation of intuitionistic number theory