# 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