Personal tools
You are here: Home Events LFCS seminar: Dominic Orchard: Fine-grained program reasoning via graded modal type theories

LFCS seminar: Dominic Orchard: Fine-grained program reasoning via graded modal type theories

— filed under: ,

What
  • LFCS Seminar
  • Upcoming events
When Jun 06, 2017
from 04:00 PM to 05:00 PM
Where IF 4.31/4.33
Add event to calendar vCal
iCal

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, input-output) 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.

 

Document Actions