Dialectica categories for the lambek calculus

Valeria de Paiva, Harley Eades

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Scopus citations

Abstract

We revisit the old work of de Paiva on the models of the Lambek Calculus in dialectica models making sure that the syntactic details that were sketchy on the first version got completed and verified. We extend the Lambek Calculus with a κ modality, inspired by Yetter’s work, which makes the calculus commutative. Then we add the of-course modality !, as Girard did, to re-introduce weakening and contraction for all formulas and get back the full power of intuitionistic and classical logic. We also present the categorical semantics, proved sound and complete. Finally we show the traditional properties of type systems, like subject reduction, the Church-Rosser theorem and normalization for the calculi of extended modalities, which we did not have before.

Original languageEnglish (US)
Title of host publicationLogical Foundations of Computer Science - International Symposium, LFCS 2018, Proceedings
EditorsAnil Nerode, Sergei Artemov
PublisherSpringer Verlag
Pages256-272
Number of pages17
ISBN (Print)9783319720555
DOIs
Publication statusPublished - Jan 1 2018
EventInternational Symposium on Logical Foundations of Computer Science, LFCS 2018 - [state] FL, United States
Duration: Jan 8 2018Jan 11 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10703 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

OtherInternational Symposium on Logical Foundations of Computer Science, LFCS 2018
CountryUnited States
City[state] FL
Period1/8/181/11/18

    Fingerprint

Keywords

  • Categorical semantics
  • Dialectica models
  • Lambek calculus
  • Linear logic
  • Non-commutative
  • Structural rules
  • Type theory

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

de Paiva, V., & Eades, H. (2018). Dialectica categories for the lambek calculus. In A. Nerode, & S. Artemov (Eds.), Logical Foundations of Computer Science - International Symposium, LFCS 2018, Proceedings (pp. 256-272). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10703 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-72056-2_16