A Fibrational Framework for Substructural and Modal Logics

Authors Daniel R. Licata, Michael Shulman, Mitchell Riley



PDF
Thumbnail PDF

File

LIPIcs.FSCD.2017.25.pdf
  • Filesize: 0.59 MB
  • 22 pages

Document Identifiers

Author Details

Daniel R. Licata
Michael Shulman
Mitchell Riley

Cite AsGet BibTex

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)
https://doi.org/10.4230/LIPIcs.FSCD.2017.25

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.
Keywords
  • type theory
  • modal logic
  • substructural logic
  • homotopy type theory

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Andreas Abel. The next 700 modal type assignment systems. In International Conference on Types for Proofs and Programs (TYPES), 2015. Google Scholar
  2. Thorsten Altenkirch and Ambrus Kaposi. Type theory in type theory using quotient inductive types. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016. Google Scholar
  3. Robert Atkey. A λ-calculus for resource separation. In Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, volume 3142 of Lecture Notes in Computer Science, pages 158-170. Springer, 2004. Google Scholar
  4. Nuel D. Belnap Jr. Display logic. Journal of Philosophical Logic, 11:375-417, 1982. Google Scholar
  5. Nick Benton. A mixed linear and non-linear logic: Proofs, terms and models. In Computer Science Logic, volume 933 of LNCS. Springer-Verlag, 1995. Google Scholar
  6. Nick Benton and Philip Wadler. Linear logic, monads and the lambda calculus. In IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 1996. Google Scholar
  7. G. Bierman and V.C.V. de Paiva. On an intuitionistic modal logic. Studia Logica, 65:383-416, 2000. Google Scholar
  8. Iliano Cervesato and Frank Pfenning. A linear logical framework. Information and Computation, 179(1):19-75, 2002. Google Scholar
  9. Karl Crary. Higher-order representation of substructural logics. In ACM SIGPLAN International Conference on Functional Programming, pages 131-142. ACM, 2010. Google Scholar
  10. Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. The structure of exponentials: Uncovering the dynamics of linear logic proofs. In Kurt Godel Colloquium, LNCS, pages 159-171. Springer, 1993. Google Scholar
  11. Neil Ghani, Patricia Johann, Fredrik Nordvall Forsberg, Federico Orsanigo, and Tim Revell. Bifibrational functorial semantics for parametric polymorphism. In Proceedings of Mathematical Foundations of Program Semantics, 2015. Google Scholar
  12. Claudio Hermida. Fibrations for abstract multicategories. Fields Institute Communications; available from http://sqig.math.ist.utl.pt/pub/HermidaC/fib-mul.pdf , 2002.
  13. Fritz Hörmann. Fibered multiderivators and (co)homological descent. Available from http://arxiv.org/abs/1505.00974, 2015.
  14. Joachim Lambek. The mathematics of sentence structure. The American Mathematical Monthly, 65:154-170, 1958. Google Scholar
  15. Daniel R. Licata and Michael Shulman. Adjoint logic with a 2-category of modes. In Logical Foundations of Computer Science, 2016. Google Scholar
  16. Daniel R. Licata, Michael Shulman, and Mitchell Riley. A fibrational framework for substructural and modal logics (extended version). Available from http://dlicata.web.wesleyan.edu/, 2017.
  17. Conor McBride. I got plenty o' nuttin'. A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, pages 207-233, 2016. Google Scholar
  18. Paul-André Meliès and Noam Zeilberger. Functors are type refinement systems. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015. Google Scholar
  19. Paul-André Meliès and Noam Zeilberger. A bifibrational reconstruction of lawvere’s presheaf hyperdoctrine. In IEEE Symposium on Logic in Computer Science, 2016. Google Scholar
  20. Vivek Nigam and Dale Miller. Algorithmic specifications in linear logic with subexponentials. In Principles and Practice of Declarative Programming, 2009. Google Scholar
  21. Peter W. O'Hearn and David J. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215-244, 1999. Google Scholar
  22. Frank Pfenning. A structural proof of cut elimination and its representation in a logical framework. Technical Report CMU-CS-94-218, Department of Computer Science, Carnegie Mellon University, 1994. Google Scholar
  23. Frank Pfenning and Rowan Davies. A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science, 11:511-540, 2001. Google Scholar
  24. Jason Reed. Names are (mostly) useless: Encoding nominal logic programming techniques with use-counting and dependent types. Talk at Working on Mechanizing Metatheory (WMM), 2008. Google Scholar
  25. Jason Reed. A Hybrid Logical Framework. PhD thesis, Carnegie Mellon University, 2009. Google Scholar
  26. Jason Reed. A judgemental deconstruction of modal logic. Available from https://www.cs.cmu.edu/~jcreed/papers/jdml.pdf, 2009.
  27. Jason Reed and Frank Pfenning. A constructive approach to the resource semantics of substructural logics. Available from http://www.cs.cmu.edu/~jcreed/papers/rp-substruct.pdf, 2009.
  28. Greg Restall. An introduction to substructural logics. Routledge, 2000. Google Scholar
  29. Urs Schreiber. Differential cohomology in a cohesive infinity-topos. arXiv, 2013. URL: http://arxiv.org/abs/1310.7930.
  30. Urs Schreiber and Michael Shulman. Quantum gauge field theory in cohesive homotopy type theory. In Workshop on Quantum Physics and Logic, 2012. Google Scholar
  31. Michael Shulman. Brouwer’s fixed-point theorem in real-cohesive homotopy type theory. arXiv:1509.07584, 2015. Google Scholar
  32. Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations Of Mathematics. Available from https://homotopytypetheory.org/book, 2013.
  33. Vladimir Voevodsky. A very short note on homotopy λ-calculus. http://www.math.ias.edu/vladimir/files/2006_09_Hlambda.pdf, September 2006.
  34. Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. A concurrent logical framework I: Judgments and properties. Technical Report CMU-CS-02-101, Department of Computer Science, Carnegie Mellon University, 2002. Revised May 2003. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail