Light types for polynomial time computation in lambda calculus

DOI10.1016/j.ic.2008.08.005zbMath1169.68010OpenAlexW1989132974MaRDI QIDQ1004289

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

zbMATH Keywords

linear logictype systemlambda calculusimplicit computational complexitypolynomial time complexitylight linear logic

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Combinatory logic and lambda calculus (03B40)

Related Items

Higher-order interpretations and program complexity, Computation by interaction for space-bounded functional programming, A type assignment for \(\lambda\)-calculus complete both for FPTIME and strong normalization, Modular Inference of Linear Types for Multiplicity-Annotated Arrows, Parsimonious Types and Non-uniform Computation, Paths-based criteria and application to linear logic subsystems characterizing polynomial time, Non-linearity as the Metric Completion of Linearity, On Paths-Based Criteria for Polynomial Time Complexity in Proof-Nets, Light affine lambda calculus and polynomial time strong normalization, Light linear logics with controlled weakening: expressibility, confluent strong normalization, Light logics and optimal reduction: completeness and complexity, Complete and tractable machine-independent characterizations of second-order polytime, Linear dependent types in a call-by-value scenario, Unnamed Item, Light Linear Logic with Controlled Weakening, Polynomial time over the reals with parsimony, Light types for polynomial time computation in lambda calculus, Unary Resolution: Characterizing Ptime, Type Inference for a Polynomial Lambda Calculus, Strong normalization of \(\mathsf{ML}^{\mathsf F}\) via a calculus of coercions, Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs, Proof-Theoretic Semantics and Feasibility, On the expressivity of elementary linear logic: characterizing Ptime and an exponential time hierarchy, Implicit computation complexity in higher-order programming languages

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Type inference for light affine logic via constraints on words
• Light affine lambda calculus and polynomial time strong normalization
• 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
• On an intuitionistic modal logic
• Stratified coherence spaces: A denotational semantics for light linear logic
• Soft linear logic and polynomial time
• On an interpretation of safe recursion in light affine logic
• Light affine set theory: A naive set theory of polynomial time
• Static prediction of heap space usage for first-order functional programs
• Linear logic and polynomial time
• Verification of Ptime Reducibility for System F Terms Via Dual Light Affine Logic
• Classical linear logic of implications
• Optimizing optimal reduction
• Verification of Ptime Reducibility for system F Terms: Type Inference in Dual Light Affine Logic
• Typed Lambda Calculi and Applications
• Typed Lambda Calculi and Applications
• Intuitionistic Light Affine Logic
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science