2007/10/05 by Dominique Duval, Duval, Dominique · 1 citation
Computer Science · #Category Theory (math.CT) #FOS: Computer and information sciences #FOS: Mathematics #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.0710.1208
openalex publication_date 2007/10/05 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Diagrammatic logics were introduced in 2002, with emphasis on the notions of specifications and models. In this paper we improve the description of the inference process, which is seen as a Yoneda functor on a bicategory of fractions. A diagrammatic logic is defined from a morphism of limit sketches (called a propagator) which gives rise to an adjunction, which in turn determines a bicategory of fractions. The propagator, the adjunction and the bicategory provide respectively the syntax, the models and the inference process for the logic. Then diagrammatic logics and their morphisms are applied to the semantics of side effects in computer languages.