Expressing computational complexity in constructive type theory

DOI10.1007/3-540-60178-3_82OpenAlexW1523613085MaRDI QIDQ6064279

Robert L. Constable

Publication date: 12 December 2023

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-60178-3_82

zbMATH Keywords

computational complexitytype theoryinductive definitionprogramming logicdependent product

Mathematics Subject Classification ID

Mathematical logic and foundations (03-XX)

Cites Work

• 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
• Bounded linear logic: A modular approach to polynomial-time computability
• A new recursion-theoretic characterization of the polytime functions
• Polynomial and abstract subrecursive classes
• Functions over free algebras definable in the simply typed lambda calculus
• Proofs as programs
• The Type Theory of PL/CV3
• Data Types as Lattices
• A simple and powerful approach for studying constructivity, computability, and complexity
• On the Computational Complexity of Algorithms
• A Machine-Independent Theory of the Complexity of Recursive Functions
• Recursive objects in all finite types
• Inductively defined types in the Calculus of Constructions