Linear types and non-size-increasing polynomial time computation.

DOI10.1016/S0890-5401(03)00009-9zbMath1054.68065OpenAlexW2010059824MaRDI QIDQ1401943

Martin Hofmann

Publication date: 19 August 2003

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

Full work available at URL: https://doi.org/10.1016/s0890-5401(03)00009-9

zbMATH Keywords

Complexity theoryResourcesHigher-order functionLinear typesType system

Mathematics Subject Classification ID

Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15)

Related Items

Higher-order interpretations and program complexity ⋮ Bounded combinatory logic and lower complexity ⋮ A Short Introduction to Implicit Computational Complexity ⋮ A Categorical Setting for Lower Complexity ⋮ Non-linearity as the Metric Completion of Linearity ⋮ On quasi-interpretations, blind abstractions and implicit complexity ⋮ Algorithmically broad languages for polynomial time and space ⋮ Safe recursion revisited. I: Categorical semantics for lower complexity ⋮ Types for complexity of parallel computation in pi-calculus ⋮ Combining linear logic and size types for implicit complexity ⋮ Gödel's system \(\mathcal T\) revisited ⋮ Realizability models and implicit complexity ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Two algorithms in search of a type-system ⋮ Polynomial time over the reals with parsimony ⋮ Light types for polynomial time computation in lambda calculus ⋮ Unbounded recursion and non-size-increasing functions ⋮ Bounded Linear Logic, Revisited ⋮ Some Complexity and Expressiveness Results on Multimodal and Stratified Proof Nets ⋮ Stratified coherence spaces: A denotational semantics for light linear logic ⋮ Realizability models for BLL-like languages ⋮ On an interpretation of safe recursion in light affine logic ⋮ Implicit characterizations of FPTIME and NC revisited ⋮ Proof-Theoretic Semantics and Feasibility ⋮ On the expressivity of elementary linear logic: characterizing Ptime and an exponential time hierarchy ⋮ An abstract approach to stratification in linear logic ⋮ The Power of Closed Reduction Strategies ⋮ Program equivalence in linear contexts ⋮ Two decades of automatic amortized resource analysis ⋮ Implicit computation complexity in higher-order programming languages

Cites Work

• Unnamed Item
• Region-based memory management
• A new recursion-theoretic characterization of the polytime functions
• Light linear logic
• Safe recursion with higher types and BCK-algebra
• Static prediction of heap space usage for first-order functional programs
• The strength of non-size increasing computation
• A syntactical analysis of non-size-increasing polynomial time computation

This page was built for publication: Linear types and non-size-increasing polynomial time computation.