Pages that link to "Item:Q5957850"
From MaRDI portal
The following pages link to Refined program extraction from classical proofs (Q5957850):
Displaying 22 items.
- Negative translations not intuitionistically equivalent to the usual ones (Q361872) (← links)
- Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control (Q444460) (← links)
- A complexity analysis of functional interpretations (Q557798) (← links)
- Light Dialectica revisited (Q636373) (← links)
- Extraction of expansion trees (Q670704) (← links)
- From constructivism to computer science (Q1274450) (← links)
- Eliminating disjunctions by disjunction elimination (Q1688959) (← links)
- Uniform Heyting arithmetic (Q1772775) (← links)
- Extraction and verification of programs by analysis of formal proofs (Q1823656) (← links)
- Getting results from programs extracted from classical proofs (Q1882897) (← links)
- Programs from proofs using classical dependent choice (Q2482844) (← links)
- Refined program extraction from classical proofs: Some case studies (Q2752052) (← links)
- Practical program extraction from classical proofs (Q2852367) (← links)
- Light Dialectica program extraction from a classical Fibonacci proof (Q2864211) (← links)
- Refinement of classical proofs for program extraction (Q2876077) (← links)
- Light monotone Dialectica methods for proof mining (Q3184220) (← links)
- 2004 Annual Meeting of the Association for Symbolic Logic (Q3370628) (← links)
- Extraction of a program from deduction and its regularity. I (Q3726113) (← links)
- The greatest common divisor: A case study for program extraction from classical proofs (Q4647568) (← links)
- (Q5028422) (← links)
- Classical Extraction in Continuation Models (Q5369478) (← links)
- Program extraction from classical proofs (Q6064277) (← links)
