Light types for polynomial time computation in lambda calculus
From MaRDI portal
Publication:1004289
DOI10.1016/J.IC.2008.08.005zbMATH Open1169.68010OpenAlexW1989132974MaRDI QIDQ1004289FDOQ1004289
Authors: Patrick Baillot, Kazushige Terui 
Publication date: 2 March 2009
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.ic.2008.08.005
Recommendations
- From Proof-Nets to Linear Logic Type Systems for Polynomial Time Computing
- Light affine lambda calculus and polynomial time strong normalization
- Verification of Ptime Reducibility for System F Terms Via Dual Light Affine Logic
- Foundations of Software Science and Computation Structures
- scientific article; zbMATH DE number 512786
implicit computational complexitylinear logiclambda calculustype systempolynomial time complexitylight linear logic
Analysis of algorithms and problem complexity (68Q25) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)
Cites Work
- On an intuitionistic modal logic
- Light types for polynomial time computation in lambda calculus
- A new recursion-theoretic characterization of the polytime functions
- Light linear logic
- Linear types and non-size-increasing polynomial time computation.
- Safe recursion with higher types and BCK-algebra
- Soft linear logic and polynomial time
- Elementary complexity and geometry of interaction
- Title not available (Why is that?)
- Title not available (Why is that?)
- Verification of Ptime Reducibility for system F Terms: Type Inference in Dual Light Affine Logic
- Intuitionistic light affine logic
- Light affine lambda calculus and polynomial time strong normalization
- Title not available (Why is that?)
- On an interpretation of safe recursion in light affine logic
- Light affine set theory: A naive set theory of polynomial time
- Linear logic and polynomial time
- Verification of Ptime Reducibility for System F Terms Via Dual Light Affine Logic
- Title not available (Why is that?)
- Stratified coherence spaces: A denotational semantics for light linear logic
- FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
- Title not available (Why is that?)
- Optimizing optimal reduction
- Typed Lambda Calculi and Applications
- Typed Lambda Calculi and Applications
- Static prediction of heap space usage for first-order functional programs
- Type inference for light affine logic via constraints on words
- Classical linear logic of implications
Cited In (33)
- Foundations of Software Science and Computation Structures
- Proof-theoretic semantics and feasibility
- Modular inference of linear types for multiplicity-annotated arrows
- Light linear logics with controlled weakening: expressibility, confluent strong normalization
- Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs
- A type assignment for \(\lambda\)-calculus complete both for FPTIME and strong normalization
- Computation by interaction for space-bounded functional programming
- Higher-order interpretations and program complexity
- On the expressivity of elementary linear logic: characterizing Ptime and an exponential time hierarchy
- Verification of Ptime Reducibility for system F Terms: Type Inference in Dual Light Affine Logic
- Linear dependent types in a call-by-value scenario
- Light affine lambda calculus and polynomial time strong normalization
- Light types for polynomial time computation in lambda calculus
- Implicit computation complexity in higher-order programming languages
- A tier-based typed programming language characterizing feasible functionals
- Paths-based criteria and application to linear logic subsystems characterizing polynomial time
- A type system for PSPACE derived from light linear logic
- On paths-based criteria for polynomial time complexity in proof-nets
- A polytime functional language from light linear logic
- Complete and tractable machine-independent characterizations of second-order polytime
- Parsimonious types and non-uniform computation
- Algebras and coalgebras in the light affine lambda calculus
- Light logics and optimal reduction: completeness and complexity
- Strong normalization of \(\mathsf{ML}^{\mathsf F}\) via a calculus of coercions
- A syntactical analysis of non-size-increasing polynomial time computation
- Polynomial time calculi.
- Light Linear Logic with Controlled Weakening
- Verification of Ptime Reducibility for System F Terms Via Dual Light Affine Logic
- Non-linearity as the metric completion of linearity
- Type Inference for a Polynomial Lambda Calculus
- Polynomial Time in the Parametric Lambda Calculus.
- Polynomial time over the reals with parsimony
- Unary resolution: characterizing \textsc{Ptime}
This page was built for publication: Light types for polynomial time computation in lambda calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1004289)
