Abstract: This paper describes how a formal semantics for a computer hardware design and description language may be embedded in a proof system. An abstraction of ELLA, its formal structured operational semantics and the underlying semantic model are introduced. The LAMBDA proof system, the embedding of the semantics and some results are discussed. Some examples are shown, and other approaches are briefly surveyed.
LFCS report ECS-LFCS-91-155
This report is available in the following formats:Previous | Index | Next