1 Search Results for "Riley, Mitchell"

Document

DOI: 10.4230/LIPIcs.FSCD.2017.25

A Fibrational Framework for Substructural and Modal Logics

Authors: Daniel R. Licata, Michael Shulman, and Mitchell Riley

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract

We define a general framework that abstracts the common features of many intuitionistic substructural and modal logics / type theories. The framework is a sequent calculus / normal-form type theory parametrized by a mode theory, which is used to describe the structure of contexts and the structural properties they obey. In this sequent calculus, the context itself obeys standard structural properties, while a term, drawn from the mode theory, constrains how the context can be used. Product types, implications, and modalities are defined as instances of two general connectives, one positive and one negative, that manipulate these terms. Specific mode theories can express a range of substructural and modal connectives, including non-associative, ordered, linear, affine, relevant, and cartesian products and implications; monoidal and non-monoidal functors, (co)monads and adjunctions; n-linear variables; and bunched implications. We prove cut (and identity) admissibility independently of the mode theory, obtaining it for many different logics at once. Further, we give a general equational theory on derivations / terms that, in addition to the usual beta/eta-rules, characterizes when two derivations differ only by the placement of structural rules. Additionally, we give an equivalent semantic presentation of these ideas, in which a mode theory corresponds to a 2-dimensional cartesian multicategory, the framework corresponds to another such multicategory with a functor to the mode theory, and the logical connectives make this into a bifibration. Finally, we show how the framework can be used both to encode existing existing logics / type theories and to design new ones.

Cite as

Daniel R. Licata, Michael Shulman, and Mitchell Riley. A Fibrational Framework for Substructural and Modal Logics. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 25:1-25:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{licata_et_al:LIPIcs.FSCD.2017.25,
  author =	{Licata, Daniel R. and Shulman, Michael and Riley, Mitchell},
  title =	{{A Fibrational Framework for Substructural and Modal Logics}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{25:1--25:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.25},
  URN =		{urn:nbn:de:0030-drops-77400},
  doi =		{10.4230/LIPIcs.FSCD.2017.25},
  annote =	{Keywords: type theory, modal logic, substructural logic, homotopy type theory}
}

Refine by Author
1 Licata, Daniel R.
1 Riley, Mitchell
1 Shulman, Michael

Refine by Classification

Refine by Keyword
1 homotopy type theory
1 modal logic
1 substructural logic
1 type theory

Refine by Type
1 document

Refine by Publication Year
1 2017

1 Search Results for "Riley, Mitchell"

A Fibrational Framework for Substructural and Modal Logics

Abstract

Cite as

Thanks for your feedback!

Could not send message