Types and Programs from Euler Diagrams

Type theory provides a formal basis for programming languages and can also be used to model reasoning systems such as Euler diagrams. We present, part of a simple type theory of Euler diagrams. Expressing a system of reasoning with Euler diagrams as a collection of types and operations on types (which correspond to diagrams and reasoning rules) is a first step towards embedding visually modelled constraints directly, into the type system of a programming language.