Abstract We consider intuitionistic multimodal logics with modalities satisfying axiom K and the axiom of Necessity, as well as collections of axioms for transforming, removing and splitting modalities, specified by a relation between modalities and sequences of modalities. These axioms can be used for systems of knowledge and belief, describing multiple environments of truth and their awareness of each other. We extend Gentzen’s decidable cut-free calculus to accommodate such multimodal systems, using a modal shift operation on contexts to extend the cut elimination proof in a novel way. We then adapt the inverse method to formulate a correct and complete forward proof search for these logics, which can be interpreted in a Fitch-style manner. Proof derivation is streamlined by implementing most derivations using the cut rule. The resulting proof search allows for making multiple queries, building a database of assumptions and their consequences which can be fine-tuned and updated to fit an application.

Algebras can be used to interpret the behaviour of effectful programs. In particular, we use Eilenberg-Moore algebras given over a complete lattices of truth values, which specify answers to queries about programs. The algebras can be used to formulate a quantitative logic of behavioural properties, specifying a congruent notion of program equivalence coinciding with a notion of applicative bisimilarity. Many combinations of effects can be interpreted using these algebras. In this paper, we specify a method of generically combining effects and the algebras used to interpret them. At the core of this method is the tensor of complete lattices, which combines the carrier sets of the algebras. We show that this tensor preserves complete distributivity of complete lattices. Moreover, the universal properties of this tensor can then be used to properly combine the Eilenberg-Moore algebras. We will apply this method to combine the effects of probability, global store, cost, nondeterminism, and error effects. We will then compare this method of combining effects with the more traditional method of combining equational theories using interaction laws.

The article investigates behavioural equivalence between programs in a call-by-value functional language extended with a signature of (algebraic) effect-triggering operations. Two programs are considered as being behaviourally equivalent if they enjoy the same behavioural properties. To formulate this, we define a logic whose formulas specify behavioural properties. A crucial ingredient is a collection of modalities expressing effect-specific aspects of behaviour. We give a general theory of such modalities. If two conditions, openness and decomposability , are satisfied by the modalities, then the logically specified behavioural equivalence coincides with a modality-defined notion of applicative bisimilarity, which can be proven to be a congruence by a generalisation of Howe’s method. We show that the openness and decomposability conditions hold for several examples of algebraic effects: nondeterminism, probabilistic choice, global store, and input/output.

The paper investigates behavioural equivalence between programs in a call-by-value functional language extended with a signature of (algebraic) effect-triggering operations. Two programs are considered as being behaviourally equivalent if they enjoy the same behavioural properties. To formulate this, we define a logic whose formulas specify behavioural properties. A crucial ingredient is a collection of modalities expressing effect-specific aspects of behaviour. We give a general theory of such modalities. If two conditions, openness and decomposability , are satisfied by the modalities then the logically specified behavioural equivalence coincides with a modality-defined notion of applicative bisimilarity, which can be proven to be a congruence by a generalisation of Howe’s method. We show that the openness and decomposability conditions hold for several examples of algebraic effects: nondeterminism, probabilistic choice, global store and input/output.