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

Denotational Semantics

[[pi |- E₁ E₂: theta₂]]e s =
   ([[pi |- E₁: theta₁ -> theta₂]]e) ([[pi |- E₂: theta₁]]e) s
[[pi |- E₁ E₂: theta]]e s =
   ([[pi |- E₁: tau -> theta]]e) ([[pi |- E₂: tauexp]]e s) s

[[tauexp]] = Store -> [[tau]]
[[int]] = Int_bottom
[[bool]] = Bool_bottom
[[theta₁ -> theta₂]] = (proper [[theta₁]] -> [[theta₂]])_bottom
[[{i:theta_i}_{i in I}]] = ({ i:proper [[ theta_i ]]}_{i in I})_bottom
[[intloc]] = Location_bottom
[[store]] = Store_bottom
proper D = D - { bottom}