A Categorical Semantics for Linear Logical Frameworks

DOI10.1007/978-3-662-46678-0_7zbMATH Open1461.03014arXiv1501.05016OpenAlexW1923962694MaRDI QIDQ2948554FDOQ2948554

Matthijs Vákár

Publication date: 1 October 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Abstract: A type theory is presented that combines (intuitionistic) linear types with type dependency, thus properly generalising both intuitionistic dependent type theory and full linear logic. A syntax and complete categorical semantics are developed, the latter in terms of (strict) indexed symmetric monoidal categories with comprehension. Various optional type formers are treated in a modular way. In particular, we will see that the historically much-debated multiplicative quantifiers and identity types arise naturally from categorical considerations. These new multiplicative connectives are further characterised by several identities relating them to the usual connectives from dependent type theory and linear logic. Finally, one important class of models, given by families with values in some symmetric monoidal category, is investigated in detail.

Full work available at URL: https://arxiv.org/abs/1501.05016

Mathematics Subject Classification ID

Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Theories (e.g., algebraic theories), structure, and semantics (18C10) Type theory (03B38) Traced monoidal categories, compact closed categories, star-autonomous categories (18M10)

Cited In (13)

• Title not available (Why is that?)
• Linear Dependent Type Theory for Quantum Programming Languages
• Reverse AD at higher types: pure, principled and denotationally correct
• A formal logic for formal category theory
• Equational logic and categorical semantics for multi-languages
• Dependent Types and Fibred Computational Effects
• Game semantics for dependent types
• A Classical Sequent Calculus with Dependent Types
• Logical foundations of quantitative equality
• Games for Dependent Types
• Full Lambek Hyperdoctrine: Categorical Semantics for First-Order Substructural Logics
• Title not available (Why is that?)
• Title not available (Why is that?)

This page was built for publication: A Categorical Semantics for Linear Logical Frameworks

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