Light Dialectica Program Extraction from a Classical Fibonacci Proof

DOI10.1016/j.entcs.2006.10.050zbMath1277.03057OpenAlexW2160768215MaRDI 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 mininglight Dialectica interpretationprogram extraction from proofscomplexity of extracted programscomputationally redundant contractionsGödel's functional Dialectica interpretationquantifiers without computational meaningrefined A-translations

Mathematics Subject Classification ID

Related Items (1)

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

This page was built for publication: Light Dialectica Program Extraction from a Classical Fibonacci Proof