Modal logics are beautiful and powerful because they bring "context" into reasoning, e.g., time, certainty, place, knowledge. Via the propositions-as-types paradigm, 'modal types' capture contextual and intensional features of programming. For example, the most popular class of modal types are monads: a computation of type M A interacts with the execution context (reading-writing memory, intput-ouput) to produce a value of type A; here M corresponds to the possibility modality of S4 logic. The resulting type theory can explain when a computation is pure or impure, but nothing more. What if we want to distinguish writing-only and reading-only programs separately, or understand or restrict the particular references which were were modified?
In this talk, I introduce an emerging class of logics and type theories which provide a solution to coarse granular reasoning by replacing one modality with many. These modalities form a family with some additional structure between them, which as whole is called a "graded modality". This additional structure reflects the shape of the proof rules, exposing the structure of proofs/programs in the propositions/types.
This talk will show both the broad paradigm of Graded Modal Type Theory (GMTT) and specific examples (both from the literature and new here). These will cover type theories capturing memory effects, stateful protocols, strictness, partiality, multi-stage programming, security levels, non-linearity, and proof relevance.
Cornwallis South West,
University of Kent,