Midterm Exam

As you look through these topics, keep in mind that I do not care about the specifics of Coq commands. For example, you needn’t remember that induction performs induction, but you should remember what induction does. Similarly for all other definition and proof rules.

I will not ask you to do proofs. However, I may ask you to look at a proof and describe what is happening or describe a theorem that should be proved.

• Definition Techniques
  • Defining abstract syntax with Inductive
  • Defining functions with Fixpoint
  • Defining functions/relations with inference rules
  • Defining inductive propositions and relations
• Proof Techniques
  • Induction and cases
  • Applying theorems using apply and eapply
  • Rewriting with theorems
  • Generalizing an induction hypothesis (very basic)
• Interpreter Based Semantics
  • Interpreting arithmetic expressions (Like the AE language)
  • Interpreting sequential languages (Like the COM language)
  • Defining interpreters over abstract syntax using Fixpoint
  • Defining transformations among semantics (compilers, optimizers)
  • Verifying transformations (compilers, optimizers)