Light Dialectica program extraction from a classical Fibonacci proof

DOI10.1016/J.ENTCS.2006.10.050zbMATH Open1277.03057OpenAlexW2160768215MaRDI QIDQ2864211FDOQ2864211

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

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

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)

Cites Work

• Title not available (Why is that?)
• Some logical metatheorems with applications in functional analysis
• A quadratic rate of asymptotic regularity for CAT(0)-spaces
• A new method for establishing conservativity of classical systems over their intuitionistic version
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Bounded functional interpretation
• Unifying functional interpretations
• Title not available (Why is that?)
• Logical Approaches to Computational Barriers
• Title not available (Why is that?)
• Uniform Heyting arithmetic
• Computer Science Logic
• Term rewriting for normalization by evaluation.
• The Warshall algorithm and Dickson's lemma: Two examples of realistic program extraction

Cited In (3)

• Dialectica interpretation of well-founded induction
• Computer Science Logic
• Title not available (Why is that?)

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)