Multimodal hyperdoctrines

Abstract

This paper treats type systems addressed to the semantics of recursive function classes closed under the known as safe recursion scheme. The strategy has been the introduction of an extension of former developments made for two sorts of variables which have no counterpart in the above-mentioned type systems. Since these typings make use of modal operators to perform safety, we need a suitable interpretation of multimodal systems. The main goal has been achieved through the introduction of Multimodal Hyperdoctrines whose models, obtained through categorical interpretations of Boolean Algebras with Operators, should give an account of those semantics for recursion.