Functional interpretations of feasibly constructive arithmetic
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 432703 (Why is no real title available?)
- scientific article; zbMATH DE number 3122413 (Why is no real title available?)
- scientific article; zbMATH DE number 3959364 (Why is no real title available?)
- scientific article; zbMATH DE number 4006252 (Why is no real title available?)
- scientific article; zbMATH DE number 4066875 (Why is no real title available?)
- scientific article; zbMATH DE number 65741 (Why is no real title available?)
- scientific article; zbMATH DE number 66471 (Why is no real title available?)
- scientific article; zbMATH DE number 176198 (Why is no real title available?)
- scientific article; zbMATH DE number 176200 (Why is no real title available?)
- scientific article; zbMATH DE number 3557241 (Why is no real title available?)
- scientific article; zbMATH DE number 218550 (Why is no real title available?)
- scientific article; zbMATH DE number 3993540 (Why is no real title available?)
- scientific article; zbMATH DE number 3999883 (Why is no real title available?)
- scientific article; zbMATH DE number 3275554 (Why is no real title available?)
- scientific article; zbMATH DE number 3325567 (Why is no real title available?)
- scientific article; zbMATH DE number 3073037 (Why is no real title available?)
- A feasibly constructive lower bound for resolution proofs
- Intensional interpretations of functionals of finite type I
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- Monadic Elementary Formal Systems
- Proof theory. 2nd ed
- Propositional proof systems, the consistency of first order theories and the complexity of computations
- Provably total functions of intuitionistic bounded arithmetic
- Syntactic translations and provably recursive functions
- The intractability of resolution
- The relative efficiency of propositional proof systems
- The typed lambda-calculus is not elementary recursive
- ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
Cited in
(54)- An Application of Category-Theoretic Semantics to the Characterisation of Complexity Classes Using Higher-Order Function Algebras
- A complexity analysis of functional interpretations
- 2000 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium 2000. La Sorbonne, Paris, France, July 23-31, 2000
- A Logical Autobiography
- A new “feasible” arithmetic
- 2003 Annual Meeting of the Association for Symbolic Logic
- Realizability models and implicit complexity
- A strong induction scheme that leads to polynomially computable realizations
- On two questions about feasibly constructive arithmetic
- Computation models and function algebras
- Type 2 polynomial hierarchies
- Semantics vs syntax vs computations: Machine models for type-2 polynomial-time bounded functionals
- Logics for reasoning about cryptographic constructions
- On Choice Sets and Strongly Non-Trivial Self-Embeddings of Recursive Linear Orders
- On parallel hierarchies and \(R_k^i\)
- Implicit computation complexity in higher-order programming languages
- scientific article; zbMATH DE number 176201 (Why is no real title available?)
- Tractability of cut-free Gentzen-type propositional calculus with permutation inference. II
- Theories with self-application and computational complexity.
- Bounded functional interpretation and feasible analysis
- Polynomial-time Martin-Löf type theory
- Polynomial time operations in explicit mathematics
- 2006 Annual Meeting of the Association for Symbolic Logic
- scientific article; zbMATH DE number 4066875 (Why is no real title available?)
- Interpreting classical theories in constructive ones
- scientific article; zbMATH DE number 1471977 (Why is no real title available?)
- A feasible theory of truth over combinatory algebra
- Polynomially bounded recursive realizability
- A tight relationship between generic oracles and type-2 complexity theory
- Proof complexity of non-classical logics
- A second-order system for polytime reasoning based on Grädel's theorem.
- A proof-theoretic characterization of the basic feasible functionals
- Saturated models of universal theories
- A parametrised functional interpretation of Heyting arithmetic
- The basic feasible functionals in computable analysis
- Preservation theorems for bounded formulas
- Injecting uniformities into Peano arithmetic
- Consistency proof of a fragment of PV with substitution in bounded arithmetic
- On the computational complexity of Longley's \(H\) functional
- Two algorithms in search of a type-system
- Elementary explicit types and polynomial time operations
- On feasible numbers
- Ramified Corecurrence and Logspace
- Game semantics approach to higher-order complexity
- A weak constructive second-order arithmetic with extraction of algorithms computable in polynomial time
- Expressing computational complexity in constructive type theory
- Feasible functionals and intersection of ramified types
- Provably recursive functions of constructive and relatively constructive theories
- A tier-based typed programming language characterizing feasible functionals
- scientific article; zbMATH DE number 3972855 (Why is no real title available?)
- scientific article; zbMATH DE number 6307929 (Why is no real title available?)
- Two (or three) notions of finitism
- Graded multicategories of polynomial-time realizers
- A semantic proof of polytime soundness of light affine logic
This page was built for publication: Functional interpretations of feasibly constructive arithmetic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q685962)
