Type-theoretic functional semantics :
Denotational Semantics
- For arithmetic expressions: Expr -> State -> Nat
- For boolean expressions: BExpr -> State -> Bool
- For commands: Command -> State -> State
But there is a problem with a naive definition of the denotation function
for commands...