Go backward to Typing Rules Go up to Top Go forward to Linear Type Annotation

Typing Rules

• Expression

  • p |- N: int

    p |- N: intexp

    
    

  • p |- L: intloc

    p |- @L: intexp

    
    

  • p |- E1: intexp	p |- E2: intexp
    p |-E1+E2: intexp

    
    

  • p |- E1: intexp	p |- E2: intexp
    p |-E1=E2: boolexp

    
    

  • p |- E: boolexp

    p |- not E: boolexp

    
    
  • p |- I: Texp, if (I:Texp) in p
• Location:
  • p |- loc_i: intloc
• Numeral
  • p |- n: int

Function invocation uses type assignment.