Go backward to Denotational Semantics Go up to Top Go forward to Consequences of Correspondence

The Correspondence Principle

D in Declaration
U in Any-syntax-domain
A in Actual-parameter

D ::= ...| define I₁(I₂: theta) = U
U ::= ...| invoke I(A)
A ::= N | E | C | L | D | T

• Various parameters for U-abstractions.
• Criterium whether parameter forms fit to original language?
• Correspondence Principle
  • define I₂ = U.
  • define I₁(I₂:theta) = ...in ...I₁(U).
  • Semantics of binding I₂ to U is the same.

For every abstraction form there may be a corresponding parameterization form (and vice versa) with same binding semantics.