Light affine lambda calculus and polynomial time strong normalization

DOI10.1007/S00153-007-0042-6MaRDI QIDQ877259zbMATH OpenOpenAlexFDO

Authors 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

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)

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

Cites work

• scientific article; zbMATH DE number 1670494 (Why is no real title available?)
• scientific article; zbMATH DE number 806752 (Why is no real title available?)
• scientific article; zbMATH DE number 1392281 (Why is no real title available?)
• scientific article; zbMATH DE number 1424054 (Why is no real title available?)
• A foundational delineation of poly-time
• A new recursion-theoretic characterization of the polytime functions
• Bounded linear logic: A modular approach to polynomial-time computability
• Higher type recursion, ramification and polynomial time
• Light affine logic as a programming language: a first contribution
• Light affine set theory: A naive set theory of polynomial time
• Light linear logic
• Light types for polynomial time computation in lambda calculus
• Linear logic and elementary time
• On an interpretation of safe recursion in light affine logic
• On the computational complexity of cut-elimination in linear logic.
• Phase semantics for light linear logic
• Safe recursion with higher types and BCK-algebra
• Stratified coherence spaces: A denotational semantics for light linear logic
• Typability and type checking in System F are equivalent and undecidable

Cited in

(18)

• Light types for polynomial time computation in lambda calculus
• A semantic account of strong normalization in linear logic
• A Short Introduction to Implicit Computational Complexity
• Quantum implicit computational complexity
• Implicit computation complexity in higher-order programming languages
• Polynomial time in untyped elementary linear logic
• Light linear logics with controlled weakening: expressibility, confluent strong normalization
• On the expressivity of elementary linear logic: characterizing Ptime and an exponential time hierarchy
• Foundations of Software Science and Computation Structures
• Factorization and normalization, essentially
• A By-Level Analysis of Multiplicative Exponential Linear Logic
• Type inference for light affine logic via constraints on words
• Characterizing polynomial and exponential complexity classes in elementary lambda-calculus
• Factorization in call-by-name and call-by-value calculi via linear logic
• An elementary affine \(\lambda \)-calculus with multithreading and side effects
• Intuitionistic light affine logic
• Proof-theoretic semantics and feasibility
• Light affine set theory: A naive set theory of polynomial time

Describes a project that uses

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)