Search


Volume

Author

Year

  • < Previous
  • 1
  • Next >
2 results

Multimodal Dependent Type Theory

Daniel Gratzer ; G. A. Kavvos ; Andreas Nuyts ; Lars Birkedal.
We introduce MTT, a dependent type theory which supports multiple modalities. MTT is parametrized by a mode theory which specifies a collection of modes, modalities, and transformations between them. We show that different choices of mode theory allow us to use the same type theory to compute and&nbsp;[&hellip;]
Published on July 28, 2021
Volume 17, Issue 3

Dual-Context Calculi for Modal Logic

G. A. Kavvos.
We present natural deduction systems and associated modal lambda calculi for the necessity fragments of the normal modal logics K, T, K4, GL and S4. These systems are in the dual-context style: they feature two distinct zones of assumptions, one of which can be thought as modal, and the other as&nbsp;[&hellip;]
Published on August 19, 2020
Volume 16, Issue 3
  • < Previous
  • 1
  • Next >