A complexity analysis of functional interpretations

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

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) 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
• On weak completeness of intuitionistic predicate logic
• On the interpretation of non-finitist proofs–Part II
• A new method for establishing conservativity of classical systems over their intuitionistic version
• 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
• 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
• 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
• 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
• A complexity analysis of functional interpretations
• A note on Spector's quantifier-free rule of extensionality
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (7)

• Functional translation of a calculus of capabilities
• Hybrid functional interpretations of linear and intuitionistic logic
• A complexity analysis of functional interpretations
• 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)