Dual-Context Calculi for Modal Logic

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

42 Downloads (Pure)

Abstract

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
ISBN (Electronic)978-1-5090-3018-7
ISBN (Print)978-1-5090-3019-4
DOIs
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
http://lics.siglog.org/lics17/

Conference

ConferenceThirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)
Abbreviated titleLICS
CountryIceland
CityReykjavik
Period20/06/1723/06/17
Internet address

Structured keywords

  • Programming Languages

Keywords

  • 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