scientific article; zbMATH DE number 895269
From MaRDI portal
Publication:4883280
zbMATH Open0848.03029MaRDI QIDQ4883280FDOQ4883280
Authors: Ulrich Berger 
Publication date: 1 July 1996
Title of this publication is not available (Why is that?)
Recommendations
- Refined program extraction from classical proofs
- Refined program extraction from classical proofs: Some case studies
- Programs from proofs using classical dependent choice
- Relating Classical Realizability and Negative Translation for Existential Witness Extraction
- Practical program extraction from classical proofs
functional programcomputational content of a proofextracting programs from proofs in classical arithmeticnegative realizability
General topics in the theory of software (68N01) First-order arithmetic and fragments (03F30) Intuitionistic mathematics (03F55) Functionals in proof theory (03F10)
Cited In (18)
- Relating Classical Realizability and Negative Translation for Existential Witness Extraction
- Refined program extraction from classical proofs: Some case studies
- Existential witness extraction in classical realizability and via a negative translation
- Interactive realizers: a new approach to program extraction from nonconstructive proofs
- Title not available (Why is that?)
- Classical Program Extraction in the Calculus of Constructions
- Title not available (Why is that?)
- Classical proofs as programs: how, what and why
- Programs from proofs using classical dependent choice
- Title not available (Why is that?)
- Program extraction from classical proofs
- The computational content of classical arithmetic
- Refinement of classical proofs for program extraction
- Getting results from programs extracted from classical proofs
- Typed realizability for first-order classical analysis
- Refined program extraction from classical proofs
- Title not available (Why is that?)
- Uniform Heyting arithmetic
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4883280)
