A complexity analysis of functional interpretations

DOI10.1016/J.TCS.2004.12.019zbMATH Open1096.03071OpenAlexW2104625978MaRDI QIDQ557798FDOQ557798

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

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.

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)

Cites Work

• Handbook of proof theory
• Subsystems of second order arithmetic
• On weak completeness of intuitionistic predicate logic
• On the interpretation of non-finitist proofs–Part II
• Title not available (Why is that?)
• 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?)
• 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
• Title not available (Why is that?)
• Refined program extraction from classical proofs
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Lower Bounds on Herbrand's Theorem
• On the Interpretation of Non-Finitist Proofs--Part I
• Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals
• Formalizing forcing arguments in subsystems of second-order arithmetic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen
• Extensional Gödel functional interpretation. A consistency proof of classical analysis
• Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization
• Title not available (Why is that?)
• On n-quantifier induction
• Functional interpretation of Aczel's constructive set theory
• The role of quantifier alternations in cut elimination
• On the No-Counterexample Interpretation
• Computer Science Logic
• Functional interpretations of feasibly constructive arithmetic
• Extraction and verification of programs by analysis of formal proofs
• Extracting Herbrand disjunctions by functional interpretation
• Interpretationen der Heyting-Arithmetik endlicher Typen
• Title not available (Why is that?)
• Title not available (Why is that?)
• A complexity analysis of functional interpretations
• A note on Spector's quantifier-free rule of extensionality

Cited In (14)

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

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)