Uniform Heyting arithmetic

DOI10.1016/j.apal.2004.10.006zbMath1081.03057OpenAlexW1999810448WikidataQ126372103 ScholiaQ126372103MaRDI QIDQ1772775

Ulrich Berger

Publication date: 21 April 2005

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.2004.10.006

zbMATH Keywords

extension of Heyting arithmetic in finite typesextraction of programs from proofs

Mathematics Subject Classification ID

Logic in computer science (03B70) First-order arithmetic and fragments (03F30) Structure of proofs (03F07)

Related Items

Light monotone Dialectica methods for proof mining, To be or not to be constructive, that is not the question, Light Dialectica revisited, Dialectica Interpretation with Fine Computational Control, Programs from proofs using classical dependent choice, A functional interpretation for nonstandard arithmetic, COMPUTABILITY THEORY, NONSTANDARD ANALYSIS, AND THEIR CONNECTIONS, Realizability interpretation of proofs in constructive analysis, The strength of compactness in computability theory and nonstandard analysis, Light Dialectica Program Extraction from a Classical Fibonacci Proof

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Constructivism in mathematics. An introduction. Volume II
• Total sets and objects in domain theory
• Synthesis of ML programs in the system Coq
• Classical logic, storage operators and second-order lambda-calculus
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization
• On the computational content of the axiom of choice
• A new method for establishing conservativity of classical systems over their intuitionistic version
• Refined program extraction from classical proofs