Go backward to Parameterized Abstractions Go up to Top Go forward to Parameter Forms

Typing Rules

• Abstraction:

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

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

  • pi₁ -U- pi₂ = pi₂ -U-(pi₁ - { (I:v) | (I:w) in pi₂, (I:v) in pi₁}).
  • Formal parameter cancels global identifier of same name.
• Invocation:

  • pi |- U: theta1

    pi |- invoke I(U): theta2

    if (I:theta₁ -> theta₂) in pi
  • Type of formal parameter must match type of actual parameter.
• Formal parameter reference:

  • pi |-I: theta

    if (I:theta) in pi
  • Formal parameters are referenced like abstractions (correspondence)!