Current browse context:
cs.LO
Change to browse by:
References & Citations
Computer Science > Logic in Computer Science
Title: Syntax and Semantics of Linear Dependent Types
(Submitted on 30 Apr 2014 (v1), last revised 16 Jan 2015 (this version, v4))
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.
Submission history
From: Matthijs Vákár [view email][v1] Wed, 30 Apr 2014 20:58:03 GMT (42kb)
[v2] Thu, 21 Aug 2014 22:25:08 GMT (55kb)
[v3] Tue, 7 Oct 2014 20:48:27 GMT (57kb)
[v4] Fri, 16 Jan 2015 19:28:48 GMT (61kb)
Link back to: arXiv, form interface, contact.