Go backward to Properties of Operational SemanticsGo up to TopGo forward to Design of a Language Core |

- Predicate
`comp`(computable):_{H}`comp`(_{i}ntloc*p*) :=*p*=>**v*and*v*means*l*where*l*in`Location`is the meaning of*p*.`comp`(_{T}exp*p*) :=*p(s)*=>**v*and*v*means*n*where*s*in`Store`and*p(s)*means*n*in [[]]._{T}`comp`*comm*(*p*) :=*p(s)*=>**v*and*v*means*s'*where*s*in`Store`and*p(s)*means*s'*in`Store`.

`comp`[[U:_{H}*H*]] holds for all well-typed phrases U:*H*.- Induction on typing rules.

*Computational adequacy follows from soundness of typing, soundness of
operational semantics and the computability of phrases.*

Author: Wolfgang Schreiner

Last Modification: March 26, 1998