Abstract

Basic propositional logic can be extended with the ability to reason about different modes of truth. In particular, I will discuss three different modalities: necessity, possibility, and “lax truth” (ie, truth up to an unspecified constraint). Under the Curry-Howard correspondence, these modalities (and simple extensions thereof) can be used to reason about complicated program domains such as staged computation, security, proof search, and distributed systems. In this talk, I will introduce the basics of modal logic, then discuss how it can be applied to type systems in these areas.