Stratified coherence spaces: A denotational semantics for light linear logic

DOI10.1016/J.TCS.2003.10.015MaRDI QIDQ1827389zbMATH OpenOpenAlexWikidataFDO

Authors Patrick Baillot

Publication date 6 August 2004

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2003.10.015

zbMATH Keywords

coherent spaceslight linear logiclinear logicproof-nets

Mathematics Subject Classification ID

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

Review text

The author provides a denotational model for Light Linear Logic, a weak variant of Linear Logic. The model is the category {\text {BSCOH}} of stratified measured coherent spaces (and locally bounded stratified cliques), which is considered to be a sub-category of stratified coherent spaces which is proved to be a model of Elementary Linear Logic (the analogue of Light Linear Logic for the Kalmar elementary functions). The soundness of the model with respect to Light Linear Logic is proved via proof-nets. The model {\text {BSCOH}} is not complete with respect to Light Linear Logic as it validates some extra principles; though it does not satisfy some specific principles (e.g. the iteration principle) which are included in Linear Logic but excluded in Light Linear Logic.

Recommendations

• scientific article; zbMATH DE number 1231574
• Phase semantics for light linear logic
• scientific article; zbMATH DE number 1231527
• On phase semantics and denotational semantics in multiplicative-additive linear logic
• On the categorical semantics of elementary linear logic

Cites work

• Elementary complexity and geometry of interaction
• scientific article; zbMATH DE number 1670494 (Why is no real title available?)
• scientific article; zbMATH DE number 1231574 (Why is no real title available?)
• scientific article; zbMATH DE number 1302629 (Why is no real title available?)
• scientific article; zbMATH DE number 1342272 (Why is no real title available?)
• scientific article; zbMATH DE number 1342282 (Why is no real title available?)
• scientific article; zbMATH DE number 1479606 (Why is no real title available?)
• scientific article; zbMATH DE number 786485 (Why is no real title available?)
• scientific article; zbMATH DE number 937366 (Why is no real title available?)
• scientific article; zbMATH DE number 1392281 (Why is no real title available?)
• Light linear logic
• Linear logic
• Linear logic and elementary time
• Linear types and non-size-increasing polynomial time computation.

Cited in

(15)

• Light types for polynomial time computation in lambda calculus
• Linear logic by levels and bounded time complexity
• Phase semantics for light linear logic
• Linear logic and elementary time
• Characterizing polynomial and exponential complexity classes in elementary lambda-calculus
• Realizability models for BLL-like languages
• Polynomial time in untyped elementary linear logic
• An abstract approach to stratification in linear logic
• scientific article; zbMATH DE number 1231574 (Why is no real title available?)
• A Fresh Look at the λ-Calculus
• A semantic measure of the execution time in linear logic
• Implicit computation complexity in higher-order programming languages
• On phase semantics and denotational semantics: The exponentials
• Type inference for light affine logic via constraints on words
• Light affine lambda calculus and polynomial time strong normalization

This page was built for publication: Stratified coherence spaces: A denotational semantics for light linear logic

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