Ch.2 Mathematical Preliminaries

• Induction

Ch.3 Untyped Arithmetic Expressions

3.1

• The untyped arithmetic expressions (syntax)

3.4 Semantic style

• Operational semantics : small-step semantics, big-step semantics (natural semantics)
• Denotational semantics (domain theory)
• Aximatic semantics

3.5 Evaluation (semantics, operational)

• Figure 3-1 (boolean expressions)
• Figure 3-2 (arithmetic expressions)

Ch.4 An ML Implementation of Arithmetic Expressions

• Term declaration in ML
• Evaluator in ML

Ch.8 Typed Arithmetic Expressions

• Types
• Typing rules
• Type soundness theorem
  • Progress theorem
  • Preservation theorem (Subject reduction)

Note.

• We do implement the untyped Arithmetic expression language (semantics) in Haskell.
• We observe some intuitively malformed expressions will get stuck under the implemented semantics.
• We implement the type system of the language to see that those malformed expressions can be excluded from the consideration of execution under the semantics.