Logic and Dependent Types in the Aldor Computer Algebra System

We show how the Aldor type system can represent propositions of first-order logic, by means of the ‘propositions as types’ correspondence. The representation relies on type casts (using pretend) but can be viewed as a prototype implementation of a modified type system with type evaluation reported elsewhere [9]. The logic is used to provide an axiomatisation of a number of familiar Aldor categories as well as a type of vectors.