Go backward to Variable Declarations Go up to Top Go forward to Eager Evaluation Semantics

Eager Evaluation Semantics

• Without variable declarations:
  • [[pi |- I=E: {I:theta}]]e s = {I = [[pi |- E: theta]]e s}
  • [[pi |- E₁,E₂: pi₁ U pi₂]]e s =
       ([[pi |- E₁: pi₁]]e s) union ([[pi |- E₂: pi₂]]e s)
  • [[pi |- with E₁ do E₂: theta]]e s =
       [[pi -U- pi₁ |- E₂: theta]](e -U- ([[pi |- E₁: pi₁]]e s)) s
  • [[pi |- I: theta]]e s = u, where (I=u) in e
  • [[pi |- lambdaI:theta₁. E: theta₁ -> theta₂]]e s = f
       where f u s' =
          [[pi -U- {I:theta₁} |- E: theta₂]](e -U- {I=u}) s'
  • [[pi |- E₁ E₂: theta₂]]e s =
       ([[pi |- E₁: theta₁ -> theta₂]]e)([[pi |- E₂: theta₁]]e s) s
• Type semantics:
  • [[{i:theta_i}_{i in I}]] = ({ i:eval(theta_i) }_{i in I})_bottom
  • [[theta₁ -> theta₂]] = (eval(theta₁) -> [[theta₂]])_bottom
  • [[comm]] = (Store -> Store)_bottom
  • [[tauexp]] = (Store -> [[tau]])_bottom