DIAgrammatic LOGic

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 Σ 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 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.

A major role is played by **pleomorphisms**:
for a given logic L:S->T,
a pleomorphism is "half-way" between a general morphism
and an isomorphism; it is a (generally non-reversible) morphism in the category
S which is mapped by the functor L
to an invertible morphism in the category T.
In biology, a **pleomorphism** is the occurrence of several
structural forms during the life cycle of a plant;
in diagrammatic logic, a pleomorphism refers to the occurrence of several
presentations of a given logical theory during a proof:
various lemmas are progressively added to the given axioms
until the required theorem is obtained.

- Jean-Guillaume Dumas, Dominique Duval, Laurent Fousse, Jean-Claude Reynaud. Decorated proofs for computational effects: Exceptions. Submitted for publication. arXiv:1203.2900.
- Jean-Guillaume Dumas, Dominique Duval, Laurent Fousse, Jean-Claude Reynaud. Decorated proofs for computational effects: States. Submitted for publication. arXiv:1112.2396.
- Jean-Guillaume Dumas, Dominique Duval, Laurent Fousse, Jean-Claude Reynaud. A duality between exceptions and states. Mathematical Structures for Computer Science (2012). arXiv:1112.2394.
- Cesar Dominguez, Dominique Duval. A parameterization process: from a functorial point of view. International Journal of Foundations of Computer Science 23 p.225-242 (2012). arXiv:0908.4491.
- Jean-Guillaume Dumas, Dominique Duval, Jean-Claude Reynaud. Cartesian effect categories are Freyd-categories. Journal of Symbolic Computation 46 p. 272-293 (2011) arXiv:0903.3311.
- Dominique Duval. Diagrammatic inference. arXiv:0710.1208 (2007).
- Dominique Duval. Diagrammatic Specifications. Mathematical Structures in Computer Science 13, p. 857-890 (2003).