A complexity analysis of functional interpretations

DOI10.1016/J.TCS.2004.12.019MaRDI QIDQ557798zbMATH OpenOpenAlexFDO

Authors Mircea-Dan Hernest, Ulrich Kohlenbach

Publication date 30 June 2005

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2004.12.019

zbMATH Keywords

Computational complexityCombinatorial logicFunctional interpretationFunctionals of finite typeProgram extraction from (classical) proofsProof complexityProof miningProof-carrying codeSoftware and systems verification

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Complexity of proofs (03F20) Second- and higher-order arithmetic and fragments (03F35) Functionals in proof theory (03F10)

Recommendations

• Computer Science Logic
• Quasi-linear Dialectica Extraction
• Extracting Herbrand disjunctions by functional interpretation
• A functional interpretation with state
• Analysis of methods for extraction of programs from non-constructive proofs.

Cites work

• scientific article; zbMATH DE number 440479 (Why is no real title available?)
• scientific article; zbMATH DE number 956475 (Why is no real title available?)
• scientific article; zbMATH DE number 3668590 (Why is no real title available?)
• scientific article; zbMATH DE number 3754681 (Why is no real title available?)
• scientific article; zbMATH DE number 3614784 (Why is no real title available?)
• scientific article; zbMATH DE number 1215497 (Why is no real title available?)
• scientific article; zbMATH DE number 1215500 (Why is no real title available?)
• scientific article; zbMATH DE number 481931 (Why is no real title available?)
• scientific article; zbMATH DE number 2174396 (Why is no real title available?)
• scientific article; zbMATH DE number 2110623 (Why is no real title available?)
• scientific article; zbMATH DE number 3231083 (Why is no real title available?)
• A complexity analysis of functional interpretations
• A new method for establishing conservativity of classical systems over their intuitionistic version
• A note on Spector's quantifier-free rule of extensionality
• Computer Science Logic
• Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization
• Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen
• Extensional Gödel functional interpretation. A consistency proof of classical analysis
• Extracting Herbrand disjunctions by functional interpretation
• Extraction and verification of programs by analysis of formal proofs
• Formalizing forcing arguments in subsystems of second-order arithmetic
• Functional interpretation of Aczel's constructive set theory
• Functional interpretations of feasibly constructive arithmetic
• Handbook of proof theory
• Interpretationen der Heyting-Arithmetik endlicher Typen
• Lower Bounds on Herbrand's Theorem
• Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• On n-quantifier induction
• On the Interpretation of Non-Finitist Proofs--Part I
• On the No-Counterexample Interpretation
• On the interpretation of non-finitist proofs–Part II
• On weak completeness of intuitionistic predicate logic
• Refined program extraction from classical proofs
• Subsystems of second order arithmetic
• The role of quantifier alternations in cut elimination
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES

Cited in

(14)

• A complexity analysis of functional interpretations
• The complexity space of partial functions: a connection between complexity analysis and denotational semantics
• Analysing the complexity of functional programs: higher-order meets first-order
• Gödel's functional interpretation and the concept of learning
• On the Herbrand functional interpretation
• Computer Science Logic
• Proof interpretations. Theoretical and practical aspects.
• Dialectica interpretation with marked counterexamples
• Functional translation of a calculus of capabilities
• Hybrid functional interpretations of linear and intuitionistic logic
• A functional functional interpretation
• Extracting Herbrand disjunctions by functional interpretation
• A functional interpretation with state
• Functional interpretations. From the Dialectica interpretation to interpretations of classical and constructive set theory

This page was built for publication: A complexity analysis of functional interpretations

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