Go backward to Declaration Abstractions Go up to Top Go forward to Alternative Semantics

Semantics of Declaration Abstractions

• P |- D: P1dec

  module I={D}: {I:P1dec}dec

• P |- import I: P1dec

  if (I:P1dec) in P

• [[P |- module I={D}: {I:P₁dec}dec]]e s =
      ({I=f}, s)
      where f(s') = [[P |- D: P₁dec]]e s'
• [[P |- import I: P₁dec]]e s = f(s)
      where (I=f) in e

• Lazy evaluation semantics of abstraction.
• Storage cell for module's variables not allocated until module imported.

module M = {var A: newint};
module N = {var B: newint};
import M in A:=0

Only one location is allocated!