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

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)

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

• 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

Cited in

(19)

• scientific article; zbMATH DE number 5000963 (Why is no real title available?)
• I got plenty o' nuttin'
• \textsc{Lincx}: a linear logical framework with first-class contexts
• Dependent types and fibred computational effects
• Syntax and semantics of quantitative type theory
• 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
• 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
• scientific article; zbMATH DE number 4202257 (Why is no real title available?)
• scientific article; zbMATH DE number 1512620 (Why is no real title available?)
• 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)