Download PDFOpen PDF in browser

Substructural Calculi with Dependent Types

EasyChair Preprint no. 421

7 pagesDate: August 10, 2018

Abstract

In this paper, we investigate how to introduce dependent types into the substructural calculi such as the Lambek calculus and linear logic. The motivations of such a move include facilitating a closer correspondence between syntax and semantics in natural language analysis and developing promising applications such as that to concurrency through dependent session types.

We shall present two substructural calculi with dependent types: the first containing dependent Lambek types and the second dependent linear types. Technically, the former adheres to the usual assumption that types do not depend on substructural variables (in this case, the Lambek variables), which makes the technical development easier, while the latter allows type dependency on linear variables, which makes the development more challenging as well as more interesting in applications.

Keyphrases: dependent types, Lambek calculus, linear logic, substructural calculus

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@Booklet{EasyChair:421,
  author = {Zhaohui Luo},
  title = {Substructural Calculi with Dependent Types},
  howpublished = {EasyChair Preprint no. 421},
  doi = {10.29007/qrqp},
  year = {EasyChair, 2018}}
Download PDFOpen PDF in browser