A categorical semantics for linear logical frameworks

DOI10.1007/978-3-662-46678-0_7MaRDI QIDQ2948554zbMATH OpenOpenAlexFDO

Authors Matthijs Vákár

Publication date 1 October 2015

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

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

Mathematics Subject Classification ID

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

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.

Recommendations

• scientific article; zbMATH DE number 1512620
• 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

Cited in

(23)

• Game semantics for dependent types
• Equational logic and categorical semantics for multi-languages
• Reverse AD at higher types: pure, principled and denotationally correct
• Combinatorial structure of type dependency
• Dependent types and fibred computational effects
• Full Lambek Hyperdoctrine: Categorical Semantics for First-Order Substructural Logics
• Linear types and locality
• \textsc{Lincx}: a linear logical framework with first-class contexts
• A classical sequent calculus with dependent types
• Categorical models of logical systems in the mathematical theory of programming
• I got plenty o' nuttin'
• scientific article; zbMATH DE number 4202257 (Why is no real title available?)
• scientific article; zbMATH DE number 5000963 (Why is no real title available?)
• Games for dependent types
• scientific article; zbMATH DE number 1512620 (Why is no real title available?)
• scientific article; zbMATH DE number 7204444 (Why is no real title available?)
• Syntax and semantics of quantitative type theory
• Proof-oriented categorical semantics
• A formal logic for formal category theory
• Logical foundations of quantitative equality
• Monoidal closure of Grothendieck constructions via -tractable monoidal structures and Dialectica formulas
• The quantum monadology
• Quantitative equality in substructural logic via Lipschitz doctrines

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)