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 {I$$₁=$v$₁,...,I$$_n=$v$_n}.
• Semantics of a declaration is a record.