Linear Type Annotation

See Schmidt, FIgure 2.2.

• Linear form of well-typed trees.
  • Type assignments as subscribts.
  • Type attributes as superscripts.
• Example
  • fun A=1, fun B=(@loc_1=0)
    in while B do loc_1 := (A+2) od
  • ( (fun A=((1)^int_{})^intexp_{})^{A:intexp}dec_{},
        (fun B =
        ( ((@(loc_1)^intloc_{})^intexp_{} =
        ((0)^int_{})^intexp_{})^boolexp_{})^{B:boolexp}dec_{})^p_1dec_{}
        in ( while (B)^boolexp_p do
        ((loc_1)^intloc_p:=
        ((A)^intexp_p+(2)^int_p)^intexp_p)^comm_p )^comm_p )^comm
  • p= {A: intexp, B: boolexp}