Full Language

E ::= E$$₁:=E$$₂ | E$$₁;E$$₂ | if E$$₁ then E$$₂ else E$$₃ fi
| skip | while E$$₁ do E$$₂ od | E$$₁+E$$₂ | E$$₁=E$$₂
| not E | @E | N | L
| I=E |E$$₁,E$$₂ | with E$$₁ do E$$₂ | I | lambdaI:theta. E | E$$₁ E$$₂

theta ::= tauexp | comm | intloc | pi | theta$$₁ $->$ | theta$$₂
tau ::= int | bool
pi ::= {$j$:theta$$_j}$$_{j in J}

pi |- E$$1: intloc	pi |- E$$2: intexp
pi |- E$$1:=E$$2: comm

pi |- E$$1: comm	pi |- E$$2: comm
pi |- E$$1;E$$2: comm

pi |- E$$1: boolexp	pi |- E$$2: comm	pi |- E$$3: comm
pi |- if E$$1 then E$$2 else E$$3 fi: comm

pi |- skip: comm

pi |- E$$1: boolexp	pi |- E$$2: comm
pi |- while E$$1 do E$$2 od: comm

pi |- E$$1: intexp	pi |- E$$2: intexp
pi |- E$$1+E$$2: intexp