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