Blog

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

- Defining abstract syntax with
- 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