Go backward to Denotational Semantics
Go up to Top
Go forward to Lambda Abstractions Alone

Denotational Semantics

[[pi |- E1 E2: theta2]]e s =
   ([[pi |- E1: theta1 -> theta2]]e) ([[pi |- E2: theta1]]e) s
[[pi |- E1 E2: theta]]e s =
   ([[pi |- E1: tau -> theta]]e) ([[pi |- E2: tauexp]]e s) s

[[tauexp]] = Store -> [[tau]]
[[int]] = Intbottom
[[bool]] = Boolbottom
[[theta1 -> theta2]] = (proper [[theta1]] -> [[theta2]])bottom
[[{i:thetai}i in I]] = ({ i:proper [[ thetai ]]}i in I)bottom
[[intloc]] = Locationbottom
[[store]] = Storebottom
proper D = D - { bottom}


Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: records.tex,v 1.1 1996/05/20 12:33:10 schreine Exp schreine

Prev Up Next