The provably terminating operations of the subsystem PETJ of explicit mathematics

DOI10.1016/J.APAL.2011.04.004zbMath1238.03039OpenAlexW2044649998MaRDI QIDQ639690

Juan-Miguel Gracia

Publication date: 22 September 2011

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2011.04.004

zbMATH Keywords

nonstandard modelsexplicit mathematicspolytime functions

Mathematics Subject Classification ID

Complexity of computation (including implicit computational complexity) (03D15) Abstract and axiomatic computability and recursion theory (03D75)

Related Items (4)

A feasible theory of truth over combinatory algebra ⋮ Admissible closures of polynomial time computable arithmetic ⋮ Realisability in weak systems of explicit mathematics ⋮ Applicative theories for logarithmic complexity classes

Cites Work

• A proof-theoretic characterization of the basic feasible functionals
• Generalized recursion theory II. Proceedings of the 1977 Oslo Symposium
• Polytime, combinatory logic and positive safe induction
• Theories with self-application and computational complexity.
• Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory
• Realisability in weak systems of explicit mathematics
• Elementary explicit types and polynomial time operations
• Variation on a theme of Schütte
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: The provably terminating operations of the subsystem PETJ of explicit mathematics