Diagrammatic Logic provides a new algebraic point of view about logic, which is well suited for studying computational effects in programming languages. Some aspects of theoretical computer science require the collaboration of several logics. For instance, the computational effects in a language can be described with the help of three related logics. The collaboration of several logics can be expressed thanks to morphisms in a relevant category of logics.
Diagrammatic logics are defined in terms of categories of fractions, limit sketches and locally presentable categories [Duval-Lair 2002, Duval 2003]
A diagrammatic logic is defined as a functor L with a full and faithful right adjoint R, induced by a morphism of limit sketches. The target of L is the category of theories and the source of L is the category of specifications; a specification Σ is a presentation of the theory L(Σ). There can be several descriptions of such a functor L, providing several deduction systems for generating a theory from a specification.
A model of a specification Σ with values in a theory Θ is a morphism of theories from L(Σ) to Θ, or equivalently a morphism of specifications from Σ to R(Θ). Instances and inference rules are defined as fractions with respect to the localization functor L, and an inference step as a composition of fractions. The definition of morphisms of logics follows easily, so that we get the category of DIAgrammatic LOGics.
See my Publications with César Domínguez, Jean-Guillaume Dumas, Laurent Fousse and Jean-Claude Reynaud and the short paper: