A proof-theoretic characterization of the basic feasible functionals

DOI10.1016/j.tcs.2004.08.009zbMath1086.03044OpenAlexW1973440844MaRDI QIDQ706620

Thomas Strahm

Publication date: 9 February 2005

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

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

zbMATH Keywords

proof theoryapplicative theoriesbasic feasible functionalstype-two feasibility

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Relative consistency and interpretations (03F25) Higher-type and set recursion theory (03D65)

Related Items (7)

The provably terminating operations of the subsystem PETJ of explicit mathematics ⋮ Theories with self-application and computational complexity. ⋮ A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP ⋮ Primitive recursive selection functions for existential assertions over abstract algebras ⋮ Type-two polynomial-time and restricted lookahead ⋮ Elementary explicit types and polynomial time operations ⋮ Realisability in weak systems of explicit mathematics

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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Functional interpretations of feasibly constructive arithmetic
• Constructivism in mathematics. An introduction. Volume II
• A new recursion-theoretic characterization of the polytime functions
• Polynomial and abstract subrecursive classes
• A foundational delineation of poly-time
• Semantics vs syntax vs computations: Machine models for type-2 polynomial-time bounded functionals
• Polytime, combinatory logic and positive safe induction
• Theories with self-application and computational complexity.
• Higher type recursion, ramification and polynomial time
• On characterizations of the basic feasible functionals, Part I
• A new Characterization of Type-2 Feasibility
• Logic and Computation

This page was built for publication: A proof-theoretic characterization of the basic feasible functionals