A note on complexity measures for inductive classes in constructive type theory

DOI10.1006/INCO.1998.9999zbMath0916.03039OpenAlexW1978042238MaRDI QIDQ1271558

Robert L. Constable

Publication date: 6 July 1999

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/inco.1998.9999

zbMATH Keywords

computational complexityconstructive type theorycomputable functionsrecursive functionspolynomial time complexity

Mathematics Subject Classification ID

Complexity of computation (including implicit computational complexity) (03D15) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Recursive functions and relations, subrecursive hierarchies (03D20) Second- and higher-order arithmetic and fragments (03F35)

Related Items (1)

Automated higher-order complexity analysis

Uses Software

• Coq
• Automath
• ALF
• TALx86

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
• The realm of primitive recursion
• Bounded linear logic: A modular approach to polynomial-time computability
• A new recursion-theoretic characterization of the polytime functions
• Polynomial and abstract subrecursive classes
• A foundational delineation of poly-time
• Optimality and inefficiency
• Proofs as programs
• Classes of Predictably Computable Functions
• Languages that Capture Complexity Classes
• Data Types as Lattices
• ON STEPWISE EXPLICIT SUBSTITUTION
• A simple and powerful approach for studying constructivity, computability, and complexity
• Partial Applicative Theories and Explicit Substitutions
• Explicit substitutions
• On the Computational Complexity of Algorithms
• Classes of computable functions defined by bounds on computation
• Recursive objects in all finite types
• An Overview of the Theory of Computational Complexity
• Inductively defined types in the Calculus of Constructions

This page was built for publication: A note on complexity measures for inductive classes in constructive type theory