Uniform Heyting arithmetic

DOI10.1016/J.APAL.2004.10.006MaRDI QIDQ1772775zbMATH OpenOpenAlexWikidataFDO

Authors 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) Structure of proofs (03F07) First-order arithmetic and fragments (03F30)

Recommendations

• scientific article; zbMATH DE number 895269
• Refined program extraction from classical proofs
• scientific article; zbMATH DE number 65537
• Interactive realizers: a new approach to program extraction from nonconstructive proofs
• Practical program extraction from classical proofs

Cites work

• A new method for establishing conservativity of classical systems over their intuitionistic version
• Classical logic, storage operators and second-order lambda-calculus
• Constructivism in mathematics. An introduction. Volume II
• Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization
• scientific article; zbMATH DE number 65537 (Why is no real title available?)
• scientific article; zbMATH DE number 1215498 (Why is no real title available?)
• scientific article; zbMATH DE number 1241698 (Why is no real title available?)
• scientific article; zbMATH DE number 1324438 (Why is no real title available?)
• scientific article; zbMATH DE number 512771 (Why is no real title available?)
• scientific article; zbMATH DE number 1552509 (Why is no real title available?)
• scientific article; zbMATH DE number 3216998 (Why is no real title available?)
• scientific article; zbMATH DE number 3320380 (Why is no real title available?)
• scientific article; zbMATH DE number 3349775 (Why is no real title available?)
• scientific article; zbMATH DE number 2222013 (Why is no real title available?)
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• On the computational content of the axiom of choice
• Refined program extraction from classical proofs
• Subsystems of second order arithmetic
• Synthesis of ML programs in the system Coq
• Total sets and objects in domain theory
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES

Cited in

(12)

• Realizability interpretation of proofs in constructive analysis
• Arithmetizing uniform NC
• To be or not to be constructive, that is not the question
• The strength of compactness in computability theory and nonstandard analysis
• Programs from proofs using classical dependent choice
• Light Dialectica program extraction from a classical Fibonacci proof
• Light monotone Dialectica methods for proof mining
• Dialectica interpretation with fine computational control
• Computability theory, nonstandard analysis, and their connections
• Light Dialectica revisited
• Uniform functional interpretations
• A functional interpretation for nonstandard arithmetic

This page was built for publication: Uniform Heyting arithmetic

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