A Many-sorted Polyadic Modal Logic

We propose a general system that combines the powerful features of modal logic and many-sorted reasoning. Its algebraic semantics leads to a many-sorted generalization of boolean algebras with operators, for which we prove the analogue of the J ' onsson-Tarski theorem. Our goal was to deepen the connections between modal logic and program verification, while also testing the expressiveness of our system by defining a small imperative language and its operational semantics.