Relational languages such as RUBY are used to derive hardware circuits from abstract specifications of their behaviour. Much reasoning is done informally in RUBY using pictorial representations of relational terms. We formalise this use of pictures in circuit design. We show that pictures naturally form a unitary pretabular allegory. Homomorphisms of pictures correspond to adding new wires or circuit comments. Two pictures are mutually homomorphic if and only if they represent equal allegorical terms. We prove soundness and completeness results which guarantee that deriving circuits using pictures does not lead to errors. We illustrate the use of pictures by deriving the ripple adder implementation from a high level, behavioural specification.>

This research brings together, in a methodical way, several approaches to giving a compositional theory of Petri nets using category theory and to the use of linear logic in specifying and reasoning about Petri nets. The authors construct categories of nets based on V.C.V. de Paiva's dialectica category models (1989) of linear logic in which they are able to exploit the structure of de Paiva's models to give constructions on categories of nets. Using a category of safe nets as an example, it is shown how this approach yields both existing and novel constructions on nets and their computational interpretation is discussed. The authors also indicate how more general categories of nets can be expressed in this framework.>