Final Exam Coverage
Big Step Semantics

Concepts:
 What is operational semantics / how is it different?
 What is bigstep semantics?
 Relationship to the evaluator/interpreter
 Inference rules: form & meaning
 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 / Betareduction
 Variable capture and Alphaconversion
 Etareduction
 Normal form
 Evaluation order
 Applicative (callbyvalue / eager evaluation)
 Normal order (callbyname / 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 Racketbased, this topic will not be on the final exam!
Axiomatic Semantics and Hoare Logic

Concepts:
 Axiomatic semantics vs. Operational semantics
 Hoare Triple: form & meaning
 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