Dual-Context Calculi for Modal Logic

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)

43 Downloads (Pure)


We show how to derive natural deduction systems for the necessity fragment of various constructive modal logics by exploiting a pattern found in sequent calculi. The resulting systems are dual-context systems, in the style pioneered by Girard, Barber, Plotkin, Pfenning, Davies, and others. This amounts to a full extension of the Curry-Howard-Lambek correspondence to the necessity fragments of a constructive variant of the modal logics K, K4, GL, T, and S4. We investigate the metatheory of these calculi, as well as their categorical semantics. Finally, we speculate on their computational interpretation
Original languageEnglish
Title of host publication2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Number of pages12
VolumeAugust 2017
ISBN (Electronic)9781509030187
ISBN (Print)9781509030194
Publication statusPublished - 18 Aug 2017
EventThirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017) - Reykjavik University, Reykjavik, Iceland
Duration: 20 Jun 201723 Jun 2017
Conference number: 2017

Publication series

ISSN (Electronic)1043-6871


ConferenceThirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)
Abbreviated titleLICS
Internet address

Structured keywords

  • Programming Languages


  • modal logic
  • comonads
  • semantics
  • proof theory
  • Curry-Howard
  • lambda calculus

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

Cite this