This paper presents a formal model of the syntax and semantics of the
languages ComLisp and SIL using the PVS system. ComLisp is an
imperative subset of Common Lisp and serves both as a source and
implementation language for an inital fully correct compiler
implementation.  SIL (stack intermediate language) is the first of a
series of intermediate languages used to compile ComLisp programs into
binary Transputer machine code.  The formal semantic definitions make
use of a library of (generic) PVS theories defining the semantics of
standard constructs of imperative and functional languages.