An arithmetic for non-size-increasing polynomial-time computation

DOI10.1016/j.tcs.2003.10.023zbMath1064.03036OpenAlexW2051832719MaRDI QIDQ1827388

Ulrich Berger, Klaus Aehlig, Martin Hofmann, Helmut Schwichtenberg

Publication date: 6 August 2004

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

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

zbMATH Keywords

Lambda calculusImplicit computational complexityRealizabilityArithmeticHigher typesNon-size-increasing polynomial-time computation

Mathematics Subject Classification ID

Complexity of computation (including implicit computational complexity) (03D15) Combinatory logic and lambda calculus (03B40) Complexity of proofs (03F20)

Related Items

Modular Inference of Linear Types for Multiplicity-Annotated Arrows ⋮ Extracting a DPLL Algorithm ⋮ Algorithmically broad languages for polynomial time and space ⋮ Build your own clarithmetic I: Setup and completeness ⋮ Introduction to clarithmetic. I ⋮ An arithmetic for polynomial-time computation ⋮ Proof-Theoretic Semantics and Feasibility ⋮ Implicit computation complexity in higher-order programming languages

Cites Work

• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• Higher type recursion, ramification and polynomial time
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• The strength of non-size increasing computation
• A syntactical analysis of non-size-increasing polynomial time computation
• Intrinsic reasoning about functional programs. I: First order theories
• Unnamed Item
• Unnamed Item
• Unnamed Item