A complexity analysis of functional interpretations

DOI10.1016/J.TCS.2004.12.019zbMath1096.03071OpenAlexW2104625978MaRDI QIDQ557798

Ulrich Kohlenbach, Mircea-Dan Hernest

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) Specification and verification (program logics, model checking, etc.) (68Q60) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functionals in proof theory (03F10) Second- and higher-order arithmetic and fragments (03F35) Complexity of proofs (03F20)

Related Items (2)

Extracting Herbrand disjunctions by functional interpretation ⋮ A complexity analysis of functional interpretations

Cites Work

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

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