Go backward to Identifier Expressions Go up to Top Go forward to Semantics of Type Structures I

Type Attributes of Type Structures

• Type structures have command-like semantics:
  • When evaluated with current environment and store, it alters store and returns value that can be bound to identifier.
  • [[P |- T:Dclass]] in EnvP -> Store ->
        ([[D]] x Store)
• Range of type attributes:
  • D ::= intloc | P
  • P ::= {i:T_i}_{i in I}, where I subset Identifier
  • H ::= T | Texp | comm | D | Dclass | Pdec
  • T::= int | bool
• [[Dclass]] = Store -> ([[D]] x Store).