Syntax and Semantics of Linear Dependent Types

Reference. Syntax and Semantics of Linear Dependent Types

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.

Cite

Cite as @vakarSyntaxSemanticsLinear2015 (helia, typst) · \cite{vakarSyntaxSemanticsLinear2015} (LaTeX)

BibTeX

bibtex · 13 lines

@misc{vakarSyntaxSemanticsLinear2015,
 title = {Syntax and {Semantics} of {Linear} {Dependent} {Types}},
 author = {Vákár, Matthijs},
 year = {2015},
 url = {http://arxiv.org/abs/1405.0033},
 urldate = {2024-07-10},
 publisher = {arXiv},
 keywords = {Computer Science - Logic in Computer Science, Computer Science - Programming Languages, Mathematics - Category Theory},
 note = {arXiv:1405.0033 [cs, math]},
 month = {January},
 language = {en},
 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.}
}

hayagriva YAML (typst)

yaml · 11 lines

vakarSyntaxSemanticsLinear2015:
  type: misc
  title: Syntax and {Semantics} of {Linear} {Dependent} {Types}
  author: Vákár, Matthijs
  date: 2015-01
  publisher: arXiv
  url:
    value: http://arxiv.org/abs/1405.0033
    date: 2024-07-10
  note: arXiv:1405.0033 [cs, math]
  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.

Download: vakarSyntaxSemanticsLinear2015.bib · vakarSyntaxSemanticsLinear2015.yml

Cites 20 works (2 here)

With notes (2)

Syntax and semantics of dependent types Hofmann_1997Semantics and Logics of Computation · 1997

DOI

A general coherence result power_1989JPAA · 1989

External (18)

Quantization via linear homotopy types (2014)
Enriched indexed categories (2013)
Linear dependent types for differential privacy (2013)
Duality and traces for indexed monoidal categories (2012)
Linear dependent types in a call-by-value scenario (2012)
Linear dependent types and relative completeness (2011)
Categorical semantics of linear logic (2009)
Parametrized homotopy theory (2006)
A categorical quantum logic (2006)
An intuitionistic theory of types (1998)
A linear logical framework (1996)
Dual intuitionistic linear logic (1996)
The formulae-as-types notion of construction (1995)
On intuitionistic linear logic (1994)
Comprehension categories and the semantics of type dependency (1993)
Deductive systems and categories III. Cartesian closed categories, intuitionist propositional calculus, and combinatory logic (1972)
Equality in hyperdoctrines and comprehension schema as an adjoint functor (1970)
A formulation of the simple theory of types (1940)