Categories, Allegories, and Circuit Design

Languages based upon binary relations offer an appealing setting for constructing programs from specifications. For example, working with relations rather than functions allows specifications to be more abstract (for example, many programs have a natural specification using the converse operator on relations), and affords a natural treatment of non-determinism in specifications. In this paper we present a novel pictorial interpretation of relational terms as simple pictures of circuits, and a soundness/completeness result that allows relational equations to be proved by pictorial reasoning.

The PROSPER Toolkit

The PROSPER (Proof and Specification Assisted Design Environments) project advocates the use of toolkits which allow existing verification tools to be adapted to a more flexible format so that they may be treated as components. A system incorporating such tools becomes another component that can be embedded in an application. This paper describes the PROSPER Toolkit which enables this. The nature of communication between components is specified in a language-independent way. It is implemented in several common programming languages to allow a wide variety of tools to have access to the toolkit.