Go backward to Lazy and Eager Bindings Go up to Top Go forward to Typing Rules

Typing Rules

• Basic Rules

  • pi |- newint: intloc exp

  • pi |- E: theta

    pi |- lazy I=E: { I:theta}exp

  • pi |- E: tauexp

    pi |- eager I=E: { I:tau}exp

• with E₁ do E₂

  • pi |- E1: pi1	pi -U- pi1 |- E2: theta
    pi |- with E1 do E2: theta

  • pi |- E1: pi1exp	pi -U- pi1 |- E2: tauexp
    pi |- with E1 do E2: tauexp

    
    tau in { pi₂, store }
  • Second rule considers that evaluation of E₁ may cause side effects that must be managed by E₂.