Record Introduction Principle
Abstraction Principle
Phrases of any "semantically meaningful syntactic class" may be named.
- Names to well-formed phrases of any H.
- P |- U: H
- P |- define I=U: {I:H}dec
- Declaration biuilds phrase that is binding of a name to a value.
- Denotational semantics builds singleton set {(I=v)}.
- Compound declaration builds set
{I1=v1,...,In=vn}.
- Semantics of a declaration is a record.
Phrases of any semantically meaningful syntactic class may be components
of records.
Author: Wolfgang Schreiner
Last Modification: April 23, 1998