Final Exam Coverage

Big Step Semantics

• Concepts:

  • What is operational semantics / how is it different?
    • How is it useful?
  • What is big-step semantics?
    • Relationship to the evaluator/interpreter
  • Inference rules: form & meaning
    • Axioms
  • Evaluation relation
    • Components: syntactic objects, environments, results
  • Grammars & BNF specification
  • Simple Imperative Programming Language (IMP)
    • Syntax
    • Big step semantics rules

• Problems:

  • Writing inference rules
  • Drawing proof trees using given rules / assertions

Lambda Calculus

• Concepts:

  • Syntax & Semantics
    • Associativity & Precedence
  • Abstract Syntax Trees
  • Free / Bound variables
  • Function application / Beta-reduction
  • Variable capture and Alpha-conversion
    • Alpha-equivalence
  • Eta-reduction
  • Normal form
  • Evaluation order
    • Applicative (call-by-value / eager evaluation)
    • Normal order (call-by-name / lazy evaluation)
    • Pros/Cons
  • Boolean representation & Church numerals

• Problems:

  • Drawing & analyzing abstract syntax trees
  • Evaluation / reduction of lambda calculus expressions
    • Using existing definitions (e.g., of Church numerals / combinators)

Continuation Passing Style

• Note: since our coverage was entirely Racket-based, this topic will not be on the final exam!

Axiomatic Semantics and Hoare Logic

• Concepts:

  • Axiomatic semantics vs. Operational semantics
  • Hoare Triple: form & meaning
    • Form of assertions
  • Axiomatic semantics rules of inference for IMP
  • Strong vs. Weak assertions
  • Rule of consequence

• Problems:

  • Ranking assertions according to relative strength
  • Deriving weakest preconditions for given program & postcondition
  • Coming up with / Checking a loop invariant and proving partial correctness