Go backward to Higher-Order Programming Languages Go up to Top Go forward to Lazy Evaluation Semantics

Semantics of Records and Lambda Abstractions

• Core part of language:
  • [[pi |- L:=E: comm]]e s =
       update([[pi |- L: intloc]]e,
          [[pi |- E: intexp]]e s, s)
  • [[pi |- E₁;E₂: comm]]e s =
       [[pi |- E₂: comm]]e ([[pi |- E₁: comm]]e s)
  • [[pi |- E₁+E₂: intexp]]e s =
       plus([[pi |- E₁: intexp]]e s,
          [[pi |- E₂: intexp]]e s)
  • [[pi |- N: intexp]]e s = [[N: int]]e
  • [[pi |- loc_i: intloc]]e = loc_i
• Type semantics:
  • [[comm]] = Store -> Store_bottom
  • [[tauexp]] = Store -> [[tau]]

Addition of environment does not change meaning of core language programs.