Abstract

Modal logic is an extension of classical propositional logic with operators that can let us express modes of truth: instead of only differentiating between true and false propositions, we can talk about truth depending on some notion such as time, knowledge, possibility, etc. Until relatively recently, modal logic was the domain of logicians and philosophers (with a subfield, temporal logic, seeing wide use in formal verification since the late 1970s), but a series of developments starting with Moggi’s monadic metalanguage established its relevance in type theory, category theory, and other areas of theoretical and applied computer science. This talk introduces the axiomatic foundations of modal logic and how the axioms give rise to different philosophical interpretations of modal operators. We then develop the categorical semantics of S4 temporal modal logic, rediscovering many concepts that have been discussed in previous talks, and introducing new ideas specific to temporal modalities. Finally, we establish a nice connection between linear temporal logic and functional reactive programming, a declarative paradigm for programming interactive user interfaces.