Light Dialectica program extraction from a classical Fibonacci proof

DOI10.1016/J.ENTCS.2006.10.050MaRDI QIDQ2864211zbMATH OpenOpenAlexFDO

Authors 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 contractionsquantifiers without computational meaningrefined A-translationsGödel's functional Dialectica interpretation

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Complexity of proofs (03F20) Functionals in proof theory (03F10)

Recommendations

• Computer Science Logic
• Quasi-linear Dialectica Extraction
• Refined program extraction from classical proofs: Some case studies
• Analysis of methods for extraction of programs from non-constructive proofs.
• Dialectica interpretation with marked counterexamples

Cites work

• scientific article; zbMATH DE number 956475 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 1215497 (Why is no real title available?)
• scientific article; zbMATH DE number 2174396 (Why is no real title available?)
• scientific article; zbMATH DE number 3216998 (Why is no real title available?)
• A new method for establishing conservativity of classical systems over their intuitionistic version
• A quadratic rate of asymptotic regularity for CAT(0)-spaces
• Bounded functional interpretation
• Computer Science Logic
• Logical Approaches to Computational Barriers
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Refined program extraction from classical proofs
• Some logical metatheorems with applications in functional analysis
• Term rewriting for normalization by evaluation.
• The Warshall algorithm and Dickson's lemma: Two examples of realistic program extraction
• Uniform Heyting arithmetic
• Unifying functional interpretations
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES

Cited in

(3)

• Dialectica interpretation of well-founded induction
• Computer Science Logic
• scientific article; zbMATH DE number 7471663 (Why is no real title available?)

This page was built for publication: Light Dialectica program extraction from a classical Fibonacci proof

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2864211)