@inproceedings{b7f46e18f25244c5b75c65b76c50e8e9,
title = "Dialectica categories for the lambek calculus",
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{\textquoteright}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.",
keywords = "Categorical semantics, Dialectica models, Lambek calculus, Linear logic, Non-commutative, Structural rules, Type theory",
author = "{de Paiva}, Valeria and Harley Eades",
note = "Funding Information: Acknowledgments. The authors would like to thank the anonymous reviewers for their feedback which did make this a better paper. The second author was partially supported by the NSF grant #1565557. Publisher Copyright: {\textcopyright} Springer International Publishing AG 2018.; International Symposium on Logical Foundations of Computer Science, LFCS 2018 ; Conference date: 08-01-2018 Through 11-01-2018",
year = "2018",
doi = "10.1007/978-3-319-72056-2_16",
language = "English (US)",
isbn = "9783319720555",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "256--272",
editor = "Anil Nerode and Sergei Artemov",
booktitle = "Logical Foundations of Computer Science - International Symposium, LFCS 2018, Proceedings",
}