Mechanising execution sequence semantics in HOL
G Tredoux · Unisa Institutional Repository (University of South Africa) · 1992
The mechanization in Higher Order Logic of a general- purpose operational semantics for programming languages is described. The mechanization allows the sound derivation of Dijkstra-style axiomatic semantics. A small programming language fragment is presented as an illustration.