by B. W. Lampson 1, J. J. Horning 2 , R. L. London 3 , J. G. Mitchell" and G. J. Popek 4
April 20. 1976
This document describes the Euclid language. intended for the expression of system
programs which are to be verified.
Comments are earnestly solicited. and may be addressed to any of the authors. To facilitate
comparison with the Pascal report, maleri31 in this report which is new is printed in large
type. that which is copied f fom the P3scal report is in normal type, and material in the
Pascal report which is omitted|