### 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 language | English (US) |
---|---|

Title of host publication | Logical Foundations of Computer Science - International Symposium, LFCS 2018, Proceedings |

Editors | Anil Nerode, Sergei Artemov |

Publisher | Springer Verlag |

Pages | 256-272 |

Number of pages | 17 |

ISBN (Print) | 9783319720555 |

DOIs | |

State | Published - Jan 1 2018 |

Event | International Symposium on Logical Foundations of Computer Science, LFCS 2018 - [state] FL, United States Duration: Jan 8 2018 → Jan 11 2018 |

### Publication series

Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|

Volume | 10703 LNCS |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Other

Other | International Symposium on Logical Foundations of Computer Science, LFCS 2018 |
---|---|

Country | United States |

City | [state] FL |

Period | 1/8/18 → 1/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

*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

**Dialectica categories for the lambek calculus.** / de Paiva, Valeria; Eades, Harley.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

*Logical Foundations of Computer Science - International Symposium, LFCS 2018, Proceedings.*Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10703 LNCS, Springer Verlag, pp. 256-272, International Symposium on Logical Foundations of Computer Science, LFCS 2018, [state] FL, United States, 1/8/18. https://doi.org/10.1007/978-3-319-72056-2_16

}

TY - GEN

T1 - Dialectica categories for the lambek calculus

AU - de Paiva, Valeria

AU - Eades, Harley

PY - 2018/1/1

Y1 - 2018/1/1

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

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

KW - Categorical semantics

KW - Dialectica models

KW - Lambek calculus

KW - Linear logic

KW - Non-commutative

KW - Structural rules

KW - Type theory

UR - http://www.scopus.com/inward/record.url?scp=85039445131&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85039445131&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-72056-2_16

DO - 10.1007/978-3-319-72056-2_16

M3 - Conference contribution

AN - SCOPUS:85039445131

SN - 9783319720555

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 256

EP - 272

BT - Logical Foundations of Computer Science - International Symposium, LFCS 2018, Proceedings

A2 - Nerode, Anil

A2 - Artemov, Sergei

PB - Springer Verlag

ER -