License
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2017.25
URN: urn:nbn:de:0030-drops-77400
URL: http://drops.dagstuhl.de/opus/volltexte/2017/7740/
Go to the corresponding LIPIcs Volume Portal


Licata, Daniel R. ; Shulman, Michael ; Riley, Mitchell

A Fibrational Framework for Substructural and Modal Logics

pdf-format:
LIPIcs-FSCD-2017-25.pdf (0.6 MB)


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.

BibTeX - Entry

@InProceedings{licata_et_al:LIPIcs:2017:7740,
  author =	{Daniel R. Licata and Michael Shulman and Mitchell Riley},
  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 =	{Dale Miller},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7740},
  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}
}

Keywords: type theory, modal logic, substructural logic, homotopy type theory
Seminar: 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Issue Date: 2017
Date of publication: 21.08.2017


DROPS-Home | Fulltext Search | Imprint Published by LZI