Light affine lambda calculus and polynomial time strong normalization

DOI10.1007/s00153-007-0042-6zbMath1110.03009OpenAlexW2070983411MaRDI QIDQ877259

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

zbMATH Keywords

Lambda calculusLight logicsPolynomial time

Mathematics Subject Classification ID

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

Related Items (12)

A semantic account of strong normalization in linear logic ⋮ A Short Introduction to Implicit Computational Complexity ⋮ 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 ⋮ An Elementary Affine λ-Calculus with Multithreading and Side Effects ⋮ Type inference for light affine logic via constraints on words ⋮ Light types for polynomial time computation in lambda calculus ⋮ Quantum implicit computational complexity ⋮ 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

Uses Software

• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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
• A foundational delineation of poly-time
• Phase semantics for light linear logic
• Linear logic and elementary time
• Higher type recursion, ramification and polynomial time
• Safe recursion with higher types and BCK-algebra
• Stratified coherence spaces: A denotational 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
• LIGHT AFFINE LOGIC AS A PROGRAMMING LANGUAGE: A FIRST CONTRIBUTION
• Theoretical Computer Science

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