Go backward to Properties of Operational Semantics
Go up to Top
Go forward to Design of a Language Core

Computability of Phrases

Predicate comp_H (computable):
- comp_intloc(p) := p =>* v and v means l where l in Location is the meaning of p.
- comp_Texp(p) := p(s) =>* v and v means n where s in Store and p(s) means n in [[_T]].
- compcomm(p) := p(s) =>* v and v means s' where s in Store and p(s) means s' in Store.
comp_H[[U: 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.

Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: core.tex,v 1.3 1996/02/05 10:34:52 schreine Exp schreine