Light affine lambda calculus and polynomial time strong normalization

DOI10.1007/s00153-007-0042-6zbMath1110.03009MaRDI 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 calculus; Light logics; Polynomial time

Mathematics Subject Classification ID

03B70: Logic in computer science

03D15: Complexity of computation (including implicit computational complexity)

03F05: Cut-elimination and normal-form theorems

03F52: Proof-theoretic aspects of linear logic and other substructural logics

03B40: Combinatory logic and lambda calculus

03F20: Complexity of proofs

Related Items

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

Uses Software

• Automath

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
• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item