Go backward to Typing Rules Go up to Top Go forward to Induction and Recursion

Typing Rules

• Logic assertion U:T.
  • Tree U is well typed with type T.
• Static typing for language.
  • Type attributes can be calculated without evaluating the program.
• Strongly typed language.
  • No run-time incompatibility errors.
• Unicity of typing.
  • Can a syntax tree be typed in multiple ways?
• Soundness of typing rules.
  • Are the typing rules sensible in their assignment of type attributes to phrases?

Questions will be addressed later.