This section provides work of Thomas Schreiber to develop imperative programs in LEGO. Type theory tends itself naturally to proofs of functional programs, but since in practice most programs are imperative it is worthwhile to explore applications to imperative programs. We do this using Hoare logic. A difficulty is that type theory usually only allows definition of total functions, using a primitive recursion rather than general recursion, the motivation being to ensure that proofs are represented by total functions rather than partial ones. Thus the obvious technique, writing a denotation function for the imperative programs, does not work because while statements may not terminate. The choice we make is to represent expressions (which always terminate) by their denotations, and represent programs, which may not, by a data type.
As an example we take a fragment from a garbage collection algorithm on which Rod Burstall, Adriana Comagnoni and Thomas Schreiber have been working as part of a collaboration with Harlequin Ltd., who write LISP compilers amongst other products. It is a couple of loops which update an array as one scan of the marking phase.