modalities

Logic, type theory, and category theory give three equivalent ways of expressing computation. Logical theorems and axioms can be implemented as type systems for programming languages using the Curry-Howard correspondence, providing a novel means for safer code. This paper explores this connection and uses a category theory interpretation of modal logic to present an implementation of modal logic applied to distributed systems.