Go backward to Lambda Abstraction Principle Go up to Top Go forward to Summary (Semantics)

Summary (Typing Rules)

• Abstract syntax:
  • D ::= ...| define I₁(I₂: theta) = U
    U ::= ...| invoke I(V)
    V ::= ...| I
• Typing rules:

  • pi -U- {I2:theta1} |- U:theta2

    pi |- define I1(I2:theta1) = U: {I1: theta1 -> theta2 }dec

  • pi |- V: theta1

    pi |- invoke I(V): theta2

    if (I:theta₁ -> theta₂) in pi

  • pi |- I: theta

    if (I:theta) in pi
• Type attributes:
  • theta ::= tau | tauexp | comm | delta | deltaclass | pidec
       | theta₁ -> theta₂.
  • tau ::= int | bool
  • delta ::= intloc | pi
  • pi ::= {j:theta_j}_{j in J}, J subset Identifier.