Semantics of Declaration Abstractions

• $P$ |- D: $P$$$1dec

  module I={D}: {I:$P$$$1dec}dec

• $P$ |- import I: $P$$$1dec

  if (I:$P$$$1dec) in $P$

• [[$P$ |- module I={D}: {I:$P$$$₁dec}dec]]$e$ $s$ =
      ({I=$f$}, $s$)
      where $f(s\text{'})$ = [[$P$ |- D: $P$$$₁dec]]$e$ $s\text{'}$
• [[$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!