Dual-Context Calculi for Modal Logic

G. A. Kavvos*

*Corresponding author for this work

Research output: Contribution to journalArticle (Academic Journal)peer-review

8 Downloads (Pure)


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 intuitionistic. We show that these calculi have their roots in in sequent calculi. We then investigate their metatheory, equip them with a confluent and strongly normalizing notion of reduction, and show that they coincide with the usual Hilbert systems up to provability. Finally, we investigate a categorical semantics which interprets the modality as a product-preserving functor.
Original languageEnglish
Pages (from-to)10:1–10:66
Number of pages66
JournalLogical Methods in Computer Science (LMCS)
Issue number3
Publication statusPublished - 19 Aug 2020

Structured keywords

  • Programming Languages


  • modal logic
  • Curry-Howard
  • lambda calculus
  • modal type theory
  • category theory
  • categorical logic

Fingerprint Dive into the research topics of 'Dual-Context Calculi for Modal Logic'. Together they form a unique fingerprint.

Cite this