Mechanising execution sequence semantics in HOL

dc.contributor.author	Tredoux, G
dc.date.accessioned	2018-05-23T11:06:02Z
dc.date.available	2018-05-23T11:06:02Z
dc.date.issued	1992
dc.identifier.citation	Tredoux G (1992) Mechanising execution sequence semantics in HOL. The South African Computer Journal, Number 7, 1992	en
dc.identifier.issn	2313-7835
dc.identifier.uri	http://hdl.handle.net/10500/24040
dc.description.abstract	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.	en
dc.language.iso	en	en
dc.publisher	South African Computer Society (SAICSIT)	en
dc.subject	HOL	en
dc.subject	Mechanised proof	en
dc.subject	Program semantics	en
dc.subject	Weakest preconditions	en
dc.title	Mechanising execution sequence semantics in HOL	en
dc.type	Article	en