Go backward to Variable Declarations Go up to Top Go forward to Semantics of Variables

Abstract Syntax

D ::= ...| var I
C ::= L:=E | C₁;C₂ | ...
E ::= N | @L | ...
L ::= I

Example

var X; var Y; proc P = Y:=@X+1
in X:=0; call P

• Copy rule of littel use
  • Location numbers are anonymous!
• Partial application of copy rule
  • var X; var Y in X:=0; Y:=@X+1