Skip to content

Abstracts.2020.Modal

Jump to bottom
Nachi edited this page Mar 11, 2021 · 7 revisions

Modal λ-Calculi: Fitch vs. Dual-Context Style (AKA “The Fight”)

by Carlos Tomé (🔵) and Nachiappan Valliappan (🟥)

Abstract

Modal logic is an extension of propositional logic with one or more modal operators □, ◇,… sending a proposition A to a new proposition □ A, ◇ A,…. Similar to how the simply-typed λ-calculus (STLC) corresponds to propositional logic via the Curry–Howard correspondence [1], there are extensions of STLC that correspond to various modal logics, known as modal type theories. One such extension is Moggi's metalanguage [11, Table 9], which was mentioned in Carlos' talk on the semantics of computations a few weeks ago.

Modal type theories have gained traction in the last few years mainly in two different formulations. On the one hand, we have Fitch-style [2, 3] modal calculi, which have been used for reactive functional programming [4] and programming coinductive types [5], among others. On the other hand, dual-context calculi [10] have found applications in staged computation [6], information flow control (IFC) [7], and region-based memory management [8], for instance.

In this session, we will present the basic parts of these two very different modal calculi highlighting their differences and commonalities. We won't assume familiarity with modal logic, and will begin the session by briefly introducing its possible worlds semantics. This may look familiar to those of you who attended Andreas' talk on normalization by evaluation last week (more specifically, see slides 12–14 in [9]).

Resources

  1. Nachiappan Valliappan. 2021. An Implementation of Fitch-Style Intuitionistic K in Agda.
  2. Carlos Tomé and Nachiappan Valliappan. 2021. Talk recording.

References

  1. ^ Philip Wadler. 2015. Propositions as Types.
  2. ^ Ranald Clouston. 2018. Fitch-Style Modal Lambda Calculi.
  3. ^ Frederic Brenton Fitch. 1952. Symbolic logic, an introduction.
  4. ^ Patrick Bahr, Christian Graulund, and Rasmus Ejlers Møgelberg. 2019. Simply RaTT: a fitch-style modal calculus for reactive programming without space leaks.
  5. ^ Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, and Andrea Vezzosi. 2019. Guarded Cubical Type Theory.
  6. ^ Rowan Davies and Frank Pfenning. 2001. A modal analysis of staged computation.
  7. ^ Kenji Miyamoto and Atsushi Igarashi. 2004. A Modal Foundation for Secure Information Flow. FCS04 slides.
  8. ^ Mads Tofte, Lars Birkedal, Martin Elsman, and Niels Hallenberg. 2001. A Retrospective on Region-Based Memory Management.
  9. ^ Andreas Abel. 2019. Normalization by Evaluation for Call-by-Push-Value — Towards a Modal-Logical Reconstruction of NbE.
  10. ^ Georgios Alexandros Kavvos. 2020. Dual-Context Calculi for Modal Logic.
  11. ^ Eugenio Moggi. 1991. Notions of computation and monads.

Bibliography

  1. Georgios Alexandros Kavvos. 2016–?. The Many Worlds of Modal λ-calculi: I. Curry-Howard for Necessity, Possibility and Time.
Clone this wiki locally