Implementation Correctness Involving a Language with goto Statements
Bruce D. Russell · SIAM Journal on Computing · 1977
Two languages, one a simple structured programming language, the other a simple goto language, are defined. A denotational semantics is given for each language. An interpreter for the goto language is given and is proved correct with respect to the denotational semantics. A compiler from the structured to the goto language is defined and proved to be a semantically invariant translation of programs. The proofs are by computational induction.