A Categorical Semantics for Linear Logical Frameworks

Matthijs Vákár

doi:10.1007/978-3-662-46678-0_7

A Categorical Semantics for Linear Logical Frameworks

Matthijs Vákár

extern

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

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.

Original language	English
Title of host publication	Foundations of Software Science and Computation Structures
Subtitle of host publication	18th International Conference, FOSSACS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings
Editors	Andrew Pitts
Place of Publication	Berlin, Heidelberg
Publisher	Springer
Pages	102-116
Number of pages	15
Edition	1
ISBN (Electronic)	978-3-662-46678-0
ISBN (Print)	978-3-662-46677-3
DOIs	https://doi.org/10.1007/978-3-662-46678-0_7
Publication status	Published - 9 Apr 2015

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	9034

Access to Document

10.1007/978-3-662-46678-0_7

Cite this

Vákár, M. (2015). A Categorical Semantics for Linear Logical Frameworks. In A. Pitts (Ed.), Foundations of Software Science and Computation Structures: 18th International Conference, FOSSACS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings (1 ed., pp. 102-116). (Lecture Notes in Computer Science; Vol. 9034). Springer. https://doi.org/10.1007/978-3-662-46678-0_7

Vákár, Matthijs. / A Categorical Semantics for Linear Logical Frameworks. Foundations of Software Science and Computation Structures: 18th International Conference, FOSSACS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings. editor / Andrew Pitts. 1. ed. Berlin, Heidelberg : Springer, 2015. pp. 102-116 (Lecture Notes in Computer Science).

@inproceedings{16724a207d4b4926a22dee39f194e4ee,

title = "A Categorical Semantics for Linear Logical Frameworks",

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.",

author = "Matthijs V{\'a}k{\'a}r",

year = "2015",

month = apr,

day = "9",

doi = "10.1007/978-3-662-46678-0_7",

language = "English",

isbn = "978-3-662-46677-3",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "102--116",

editor = "Andrew Pitts",

booktitle = "Foundations of Software Science and Computation Structures",

edition = "1",

}

Vákár, M 2015, A Categorical Semantics for Linear Logical Frameworks. in A Pitts (ed.), Foundations of Software Science and Computation Structures: 18th International Conference, FOSSACS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings. 1 edn, Lecture Notes in Computer Science, vol. 9034, Springer, Berlin, Heidelberg, pp. 102-116. https://doi.org/10.1007/978-3-662-46678-0_7

A Categorical Semantics for Linear Logical Frameworks. / Vákár, Matthijs.
Foundations of Software Science and Computation Structures: 18th International Conference, FOSSACS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings. ed. / Andrew Pitts. 1. ed. Berlin, Heidelberg: Springer, 2015. p. 102-116 (Lecture Notes in Computer Science; Vol. 9034).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - A Categorical Semantics for Linear Logical Frameworks

AU - Vákár, Matthijs

PY - 2015/4/9

Y1 - 2015/4/9

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-662-46678-0_7

DO - 10.1007/978-3-662-46678-0_7

M3 - Conference contribution

SN - 978-3-662-46677-3

T3 - Lecture Notes in Computer Science

SP - 102

EP - 116

BT - Foundations of Software Science and Computation Structures

A2 - Pitts, Andrew

PB - Springer

CY - Berlin, Heidelberg

ER -

Vákár M. A Categorical Semantics for Linear Logical Frameworks. In Pitts A, editor, Foundations of Software Science and Computation Structures: 18th International Conference, FOSSACS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings. 1 ed. Berlin, Heidelberg: Springer. 2015. p. 102-116. (Lecture Notes in Computer Science). doi: 10.1007/978-3-662-46678-0_7

A Categorical Semantics for Linear Logical Frameworks

Abstract

Publication series

Access to Document

Fingerprint

Cite this