Light Dialectica Program Extraction from a Classical Fibonacci Proof
From MaRDI portal
Publication:2864211
DOI10.1016/j.entcs.2006.10.050zbMath1277.03057MaRDI QIDQ2864211
Publication date: 6 December 2013
Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.entcs.2006.10.050
proof mining; light Dialectica interpretation; program extraction from proofs; complexity of extracted programs; computationally redundant contractions; Gödel's functional Dialectica interpretation; quantifiers without computational meaning; refined A-translations
03B70: Logic in computer science
03B35: Mechanization of proofs and logical operations
03F10: Functionals in proof theory
03F20: Complexity of proofs
Related Items
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A quadratic rate of asymptotic regularity for CAT(0)-spaces
- Unifying functional interpretations
- Term rewriting for normalization by evaluation.
- The Warshall algorithm and Dickson's lemma: Two examples of realistic program extraction
- Uniform Heyting arithmetic
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- Bounded functional interpretation
- ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
- A new method for establishing conservativity of classical systems over their intuitionistic version
- Some logical metatheorems with applications in functional analysis
- Computer Science Logic
- Logical Approaches to Computational Barriers
- Refined program extraction from classical proofs