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 adjunctions [Kan 1958], categories of fractions [Gabriel-Zisman 1967] and limit sketches [Ehresmann 1968] [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 S is a presentation of the theory L(S). A model of a specification S in a theory T is a morphism of theories from L(S) to T, or equivalently a morphism of specifications from S to R(T). Instances and inference rules are defined as fractions with respect to the localization L, and an inference step as a composition of fractions. A morphism from a logic L to a logic L' is a pair of left adjoint functors which form a commutative square with L and L', induced by a commutative square of limit sketches. This yields the category of DIAgrammatic LOGics.

Jean-Guillaume Dumas, Dominique Duval, Laurent Fousse, Jean-Claude Reynaud. States and exceptions considered as dual effects. [hal-00445873] arXiv:1001.1662 (new version, 2011) Submitted for publication.

[Duval 2007] Dominique Duval. Diagrammatic inference. http://arxiv.org/abs/0710.1208 (2007). 

[Duval-Lair 2002] Version préliminaire : D. Duval, C. Lair. Diagrammatic Specifications. Rapport de Recherche IMAG-LMC 1043 M (2002)