Go backward to Linear Type Annotation Go up to Top Go forward to The Semantics of Abstractions

Interpretation

• p |- U:H
  • Within context p, U has type H.
  • p₁ |- loc₁:=A+2: comm.
• Type annotations can be constructed by left-to-right post-order tree traversal.
  • While descending tree to leaves, attach type assignments to nodes.
  • While ascending tree to root, attach type attributes to nodes.
• Attribute grammars:
  • Type assignments are inherited attributes.
  • Type attributes are synthesized attributes.

Typing rules define typing algorithm!