Light logics and optimal reduction: completeness and complexity

DOI10.1016/J.IC.2010.10.002zbMath1233.03059OpenAlexW2158015668MaRDI QIDQ627123

Patrick Baillot, Ugo Dal Lago, Paolo Coppola

Publication date: 21 February 2011

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

Full work available at URL: https://doi.org/10.1016/j.ic.2010.10.002

zbMATH Keywords

linear logiclambda calculusimplicit computational complexitylight linear logicproof-netsoptimal reduction

Mathematics Subject Classification ID

Proof-theoretic aspects of linear logic and other substructural logics (03F52) Combinatory logic and lambda calculus (03B40)

Related Items (5)

On quantum lambda calculi: a foundational perspective ⋮ Plugging-in proof development environments usingLocksinLF ⋮ Is the Optimal Implementation Inefficient? Elementarily Not ⋮ (In)efficiency and reasonable cost models ⋮ Implicit computation complexity in higher-order programming languages

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Light types for polynomial time computation in lambda calculus
• The structure of multiplicatives
• Light linear logic
• Interaction combinators
• Coherence for sharing proof-nets
• Reversible, irreversible and optimal \(\lambda\)-machines
• A general theory of sharing graphs
• Parallel beta reduction is not elementary recursive
• (Optimal) duplication is not elementary recursive
• Optimality and inefficiency
• Optimizing optimal reduction
• PELCR
• Verification of Ptime Reducibility for system F Terms: Type Inference in Dual Light Affine Logic
• On light logics, uniform encodings and polynomial time
• 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 logics and optimal reduction: completeness and complexity