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 (10)

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

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Uniform Heyting arithmetic