Go backward to Proof of Correspondence Go up to Top Go forward to Typing of Parameter Lists

Parameter Lists

• Bind multiple values to multiple names.
  • define I(I₁: theta₁, I₂: theta₂, ..., I_n: theta_n) = U
  • invoke I(V₁, V₂, ..., V_n)
• Sample syntax:
  • D ::= ...| define I(FL)=U
    FL ::= I:theta| I:theta, FL
    U ::= ...| invoke I(AL)
    AL ::= A | A, AL
  • A bit cumbersome for writing type rules.
• Correspondence principle:
  • Binding of multiple parameters.
  • Multiple definition bindings (compound declaration)!
• Alternative syntax:
  • D ::= ...| define I(F)=U
    F ::= I:theta| F₁, F₂
    V ::= ...| invoke I(D)