Refined program extraction from classical proofs

DOI10.1016/S0168-0072(01)00073-2zbMath0992.03070WikidataQ126421658 ScholiaQ126421658MaRDI QIDQ5957850

Helmut Schwichtenberg, Ulrich Berger, Wilfried Buchholz

Publication date: 16 September 2002

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

zbMATH Keywords

program extraction\(A\)-translationdefinite formula

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Functionals in proof theory (03F10) Metamathematics of constructive systems (03F50)

Related Items (15)

Getting results from programs extracted from classical proofs ⋮ Light monotone Dialectica methods for proof mining ⋮ Negative translations not intuitionistically equivalent to the usual ones ⋮ Eliminating disjunctions by disjunction elimination ⋮ Light Dialectica revisited ⋮ Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control ⋮ Unnamed Item ⋮ Extraction of expansion trees ⋮ The greatest common divisor: A case study for program extraction from classical proofs ⋮ Programs from proofs using classical dependent choice ⋮ A complexity analysis of functional interpretations ⋮ Uniform Heyting arithmetic ⋮ 2004 Annual Meeting of the Association for Symbolic Logic ⋮ From constructivism to computer science ⋮ Light Dialectica Program Extraction from a Classical Fibonacci Proof

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A syntactic theory of sequential control
• Constructivism in mathematics. An introduction. Volume II
• The revised report on the syntactic theories of sequential control and state
• Classical logic, storage operators and second-order lambda-calculus
• The Warshall algorithm and Dickson's lemma: Two examples of realistic program extraction
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Ramsey's Theorem and the Pigeonhole Principle in Intuitionistic Mathematics
• Syntactic translations and provably recursive functions

This page was built for publication: Refined program extraction from classical proofs