A categorical semantics for linear logical frameworks

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

Authors: 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

Recommendations

• Publication:4508305
• Relating categorical semantics for intuitionistic linear logic
• scientific article; zbMATH DE number 1241699
• Categorical models of logical systems in the mathematical theory of programming
• scientific article; zbMATH DE number 1342281

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 (20)

• Title not available (Why is that?)
• I got plenty o' nuttin'
• \textsc{Lincx}: a linear logical framework with first-class contexts
• Syntax and semantics of quantitative type theory
• Dependent types and fibred computational effects
• 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
• Game semantics for dependent types
• A classical sequent calculus with dependent types
• Games for dependent types
• Proof-oriented categorical semantics
• Linear dependent type theory for quantum programming languages: extended abstract
• Logical foundations of quantitative equality
• Linear types and locality
• Full Lambek Hyperdoctrine: Categorical Semantics for First-Order Substructural Logics
• Categorical models of logical systems in the mathematical theory of programming
• Title not available (Why is that?)
• Title not available (Why is that?)
• Combinatorial structure of type dependency

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)