scientific article; zbMATH DE number 895269
From MaRDI portal
Publication:4883280
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
Cited in
(20)- Uniform Heyting arithmetic
- Getting results from programs extracted from classical proofs
- Programs from proofs using classical dependent choice
- Refined program extraction from classical proofs: Some case studies
- Refinement of classical proofs for program extraction
- Interactive realizers: a new approach to program extraction from nonconstructive proofs
- The computational content of classical arithmetic
- Existential witness extraction in classical realizability and via a negative translation
- Typed realizability for first-order classical analysis
- Classical Program Extraction in the Calculus of Constructions
- Relating Classical Realizability and Negative Translation for Existential Witness Extraction
- scientific article; zbMATH DE number 65537 (Why is no real title available?)
- scientific article; zbMATH DE number 1222925 (Why is no real title available?)
- scientific article; zbMATH DE number 1301852 (Why is no real title available?)
- scientific article; zbMATH DE number 517083 (Why is no real title available?)
- Classical proofs as programs: how, what and why
- scientific article; zbMATH DE number 2247255 (Why is no real title available?)
- Refined program extraction from classical proofs
- Program extraction from classical proofs
- Extraction of redundancy-free programs from constructive natural deduction proofs
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)
