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

Related Items (24)

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

This page was built for publication: Light types for polynomial time computation in lambda calculus