Linear Läuchli semantics

DOI10.1016/0168-0072(95)00017-8zbMath0856.03006OpenAlexW1979324214MaRDI QIDQ1919529

Richard F. Blute, Philip J. Scott

Publication date: 11 February 1997

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0168-0072(95)00017-8

zbMATH Keywords

Hopf algebrasgroup actionslogical relationsparametricityfull completenessmultiplicative linear logicnoncommutative logicdinatural transformationsfunctorial polymorphismlinear analogue of Läuchli's semantics for intuitionistic logic

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items

The shuffle Hopf algebra and noncommutative full completeness ⋮ A categorical semantics for polarized MALL ⋮ Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels ⋮ Modeling linear logic with implicit functions ⋮ Proof Nets, Coends and the Yoneda Isomorphism ⋮ Exhausting strategies, joker games and full completeness for IMLL with unit ⋮ Chu spaces as a semantic bridge between linear logic and mathematics. ⋮ Relational Models for the Lambek Calculus with Intersection and Constants ⋮ Unnamed Item ⋮ Läuchli's completeness theorem from a topos-theoretic perspective ⋮ Softness of hypercoherences and MALL full completeness ⋮ Coherent phase spaces. Semiclassical semantics ⋮ Geometrical semantics for linear logic (multiplicative fragment) ⋮ Typed lambda calculi and applications. 9th international conference, TLCA 2009, Brasilia, Brazil, July 1--3, 2009. Proceedings ⋮ \(\mathbb{Z}\)-modules and full completeness of multiplicative linear logic ⋮ Syntax vs. semantics: A polarized approach ⋮ Feedback for linearly distributive categories: Traces and fixpoints ⋮ Pregroup Grammars, Their Syntax and Semantics

Cites Work

• Linear logic
• Linear logic, coherence and dinaturality
• Functorial polymorphism
• Kripke-style models for typed lambda calculus
• Natural deduction and coherence for weakly distributive categories
• Coherence for compact closed categories
• Fully abstract models of typed \(\lambda\)-calculi
• The structure of multiplicatives
• Coherence in closed categories
• Quantales and (noncommutative) linear logic
• QUASITRIANGULAR HOPF ALGEBRAS AND YANG-BAXTER EQUATIONS
• Logical relations and the typed λ-calculus
• Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic
• Lambek's categorical proof theory and Läuchli's abstract realizability
• Games and full completeness for multiplicative linear logic
• Appendix: Separability of tensor in Chu categories of vector spaces
• Intensional interpretations of functionals of finite type I
• Mechanizing logical relations
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item