Combining linear logic and size types for implicit complexity
DOI10.1016/j.tcs.2019.09.032zbMath1433.68086OpenAlexW2976136300WikidataQ127206184 ScholiaQ127206184MaRDI QIDQ1989323
Patrick Baillot, Alexis Ghyselen
Publication date: 21 April 2020
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://drops.dagstuhl.de/opus/volltexte/2018/9676/
linear logictype systemsimplicit computational complexitypolynomial-time complexity\( \lambda \)-calculussize types
Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Proof-theoretic aspects of linear logic and other substructural logics (03F52)
Cites Work
- Unnamed Item
- Unnamed Item
- Higher-order interpretations and program complexity
- Quasi-interpretations. A way to control resources
- A new recursion-theoretic characterization of the polytime functions
- Light linear logic
- Linear types and non-size-increasing polynomial time computation.
- Linear logic and elementary time
- On the expressivity of elementary linear logic: characterizing Ptime and an exponential time hierarchy
- Linear dependent types in a call-by-value scenario
- The geometry of types
- Static prediction of heap space usage for first-order functional programs
- An Elementary Affine λ-Calculus with Multithreading and Side Effects
- A Higher-Order Characterization of Probabilistic Polynomial Time
- Characterizing Polynomial and Exponential Complexity Classes in Elementary Lambda-Calculus
- Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs
- A PolyTime Functional Language from Light Linear Logic
- Amortized Resource Analysis with Polynomial Potential
- The Power of Linear Functions
- Static determination of quantitative resource usage for higher-order programs
- Multivariate amortized resource analysis
- Typed Lambda Calculi and Applications
This page was built for publication: Combining linear logic and size types for implicit complexity
