Light Dialectica Program Extraction from a Classical Fibonacci Proof

DOI10.1016/j.entcs.2006.10.050zbMath1277.03057MaRDI QIDQ2864211

Mircea-Dan Hernest

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

zbMATH Keywords

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

Mathematics Subject Classification ID

03B70: Logic in computer science

03B35: Mechanization of proofs and logical operations

03F10: Functionals in proof theory

03F20: Complexity of proofs

Related Items

Unnamed Item

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