Light affine lambda calculus and polynomial time strong normalization

DOI10.1007/S00153-007-0042-6zbMATH Open1110.03009OpenAlexW2070983411MaRDI QIDQ877259FDOQ877259

Kazushige Terui

Publication date: 19 April 2007

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00153-007-0042-6

Recommendations

• Light types for polynomial time computation in lambda calculus
• Light linear logics with controlled weakening: expressibility, confluent strong normalization
• Linear logic and polynomial time
• Intuitionistic light affine logic
• From Proof-Nets to Linear Logic Type Systems for Polynomial Time Computing

zbMATH Keywords

Lambda calculusLight logicsPolynomial time

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Complexity of proofs (03F20) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Complexity of computation (including implicit computational complexity) (03D15)

Cites Work

• Light types for polynomial time computation in lambda calculus
• Bounded linear logic: A modular approach to polynomial-time computability
• A new recursion-theoretic characterization of the polytime functions
• Light linear logic
• Typability and type checking in System F are equivalent and undecidable
• Linear logic and elementary time
• Higher type recursion, ramification and polynomial time
• Safe recursion with higher types and BCK-algebra
• Title not available (Why is that?)
• Theoretical Computer Science
• Phase semantics for light linear logic
• On an interpretation of safe recursion in light affine logic
• Light affine set theory: A naive set theory of polynomial time
• Title not available (Why is that?)
• Title not available (Why is that?)
• Stratified coherence spaces: A denotational semantics for light linear logic
• Title not available (Why is that?)
• A foundational delineation of poly-time
• LIGHT AFFINE LOGIC AS A PROGRAMMING LANGUAGE: A FIRST CONTRIBUTION

Cited In (14)

• A semantic account of strong normalization in linear logic
• On the expressivity of elementary linear logic: characterizing Ptime and an exponential time hierarchy
• Type inference for light affine logic via constraints on words
• Light types for polynomial time computation in lambda calculus
• Implicit computation complexity in higher-order programming languages
• An Elementary Affine λ-Calculus with Multithreading and Side Effects
• Characterizing polynomial and exponential complexity classes in elementary lambda-calculus
• A By-Level Analysis of Multiplicative Exponential Linear Logic
• Factorization in call-by-name and call-by-value calculi via linear logic
• Light affine set theory: A naive set theory of polynomial time
• A Short Introduction to Implicit Computational Complexity
• Proof-Theoretic Semantics and Feasibility
• Quantum implicit computational complexity
• Factorization and normalization, essentially

Uses Software

• Automath

This page was built for publication: Light affine lambda calculus and polynomial time strong normalization

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q877259)