Natural deduction and coherence for weakly distributive categories

DOI10.1016/0022-4049(95)00159-XzbMath0858.03064MaRDI QIDQ1126244

R. A. G. Seely, Todd H. Trimble, Richard F. Blute, J. Robin B. Cockett

Publication date: 19 March 1997

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

zbMATH Keywords

monoidal categoriescoherencelinear logicproof theoryproof netsconservative extensiondecision procedure\(*\)-autonomous categoriesweakly distributive categoriesexpansion-reduction systemstwo-tensor structure

Mathematics Subject Classification ID

Related Items (44)

Bifibrations of polycategories and classical linear logic ⋮ Coherence in SMCCs and equivalences on derivations in IMML with unit ⋮ An Analytic Propositional Proof System on Graphs ⋮ Weak units, universal cells, and coherence via universality for bicategories ⋮ Categorical proof theory of classical propositional calculus ⋮ A micrological study of negation ⋮ Relations and non-commutative linear logic ⋮ Unnamed Item ⋮ Linear Läuchli semantics ⋮ A practical type theory for symmetric monoidal categories ⋮ A comparison between monoidal and substructural logics ⋮ Proof Nets, Coends and the Yoneda Isomorphism ⋮ Simple free star-autonomous categories and full coherence ⋮ Exhausting strategies, joker games and full completeness for IMLL with unit ⋮ Handsome proof-nets: Perfect matchings and cographs ⋮ Combinatorial flows as bicolored atomic flows ⋮ On categorical equivalence of Gentzen-style derivations in IMLL ⋮ Promonads and String Diagrams for Effectful Categories ⋮ Unnamed Item ⋮ On linear rewriting systems for Boolean logic and some applications to proof theory ⋮ Unnamed Item ⋮ Deep inference and probabilistic coherence spaces ⋮ On cyclic star-autonomous categories ⋮ Unnamed Item ⋮ The logic of message-passing ⋮ Unnamed Item ⋮ Weakly distributive categories ⋮ Normalization of N-graphs via sub-N-graphs ⋮ Categories for computation in context and unified logic ⋮ Linear logic, coherence and dinaturality ⋮ A Logical Basis for Quantum Evolution and Entanglement ⋮ Quantum Speedup and Categorical Distributivity ⋮ Proof nets and semi-star-autonomous categories ⋮ Softness of hypercoherences and MALL full completeness ⋮ On categorical models of classical logic and the Geometry of Interaction ⋮ Proof theory in the abstract ⋮ Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic ⋮ Transformations via Geometric Perspective Techniques Augmented with Cycles Normalization ⋮ Unnamed Item ⋮ Deep inference and expansion trees for second-order multiplicative linear logic ⋮ Feedback for linearly distributive categories: Traces and fixpoints ⋮ Order-enriched categorical models of the classical sequent calculus ⋮ Aspects of Categorical Recursion Theory ⋮ The parametric continuation monad

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• On natural transformations of distinguished functors and their superpositions in certain closed categories
• Linear logic, coherence and dinaturality
• The structure of free closed categories
• Closed categories and the theory of proofs
• The geometry of tensor calculus. I
• Bounded linear logic: A modular approach to polynomial-time computability
• The structure of multiplicatives
• Coherence in closed categories
• On MacLane's conditions for coherence of natural associativities, commutativities, etc
• Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic
• Polycategories
• The mix rule
• ! and ? – Storage as tensorial strength
• The virtues of eta-expansion

This page was built for publication: Natural deduction and coherence for weakly distributive categories