Go backward to Denotations as Rewrite RulesGo up to TopGo forward to Computability of Phrases |

- Soundness.
- If
*p*has an underlying "meaning"*m*and*p => p'*, then*p'*means*m*as well. - By definition of
*=>*.

- If
- Subject reduction.
- If
*p*has an underlying "type"*T*and*p => p'*, then*p'*has*T*as well. - By soundness of typing.

- If
- Strong typing.
- If
*p*is well-typed and*p => p'*, then*p'*contains no operator-operand incompatibilities. - By induction over computation rules.

- If
- Computational adequacy.
- A program
*p*'s underlying meaning is a proper meaning*m*, if there is some value*v*such that*p => v*and*v*means*m*.

- A program

Author: Wolfgang Schreiner

Last Modification: March 26, 1998