Final Exam

The format of the final exam will be the same as the midterm with one additional short answer question. The final is comprehensive.

The exam will start at 1:30 on May 13. I will be available to describe the exam and answer questions at that time. You will have 2.5 hours from the time you start to complete the exam. I will make the exam available for 24 hours if you choose to start later. If you do choose to start later I may not be available to answer questions.

Look through the topics carefully. There are new topics and updated topics from the midterm. Keep in mind that I do not care about the specifics of Coq commands nor do I care about precise syntax.

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 C language)
  • Defining interpreters over abstract syntax using Fixpoint
  • Defining interpreters over abstract syntax using a relation
  • Defining transformations among semantics (compilers, optimizers)
  • Verifying transformations (compilers, optimizers)
• State Transition Systems
  • Elements of a state transition system
  • Defining transition relations
  • Transitive, reflexive closure of a transition system
  • Invariants (very basic)
  • Reachability
  • Simulation and Abstraction