Final Midterm Exam

Final Midterm Exam

Date: December 7, 9:30-10:15

Topics:

• Specification
  • Inductive types
  • Non-recursive definitions
  • Fixpoint definitions
  • Theorems
  • Polymorphism and type variables
• Proof tactics
  • intros
  • induction and destruct
  • rewrite and apply
  • unfold and fold
  • simpl and reflexivity
  • inversion
  • auto
• Constructive specification
  • Defining constructors
  • Defining observers
• Specifying properties
  • preconditions
  • postconditions
  • invariants
• Specifying relations
  • Relations vs. Functions
  • Inductively defining relations
  • Specifying incomplete definitions
  • Proofs using apply and auto
• Language semantics
  • Specifying evaluation using a function
  • Specifying evaluation using a relation
  • Specifying and verifying language transformations
  • Correctness definitions
• Curry-Howard
  • Types and Theorems
  • Values and Proofs