Final Exam

Final

Available: December 5 at 5:00

Due: December 12 at 2:30

Format: Download from class website, solution may be a LaTeX generated PDF, an edited PDF, a text file, or a markdown file. Submit via email to palexand@ku.edu or Canvas.

Download: here

Source: here

Topics:

• Specification
  • Inductive types
  • Non-recursive definitions
  • Fixedpoint definitions
  • Theorems
  • Type variables and polymorphisms
  • Logic
• Proof tactics
  • intros - instantiating variables
  • induction and destruct - induction and case analysis
  • rewrite and apply - using equalities and properties
  • simpl and reflexivity - simplification and decision procedures
  • discriminate and injection - using constructed type values
  • split, right, and left - logic
  • tacticals (try, ;, etc. very basic)
• Inductive Definitions
  • Defining relations
  • Defining semantics
  • Use in proofs
• Program Correctness
  • Defining correctness properties
  • Verification styles
  • Defining language semantics
• Compiler Correctness
  • Language abstract syntax
  • Interpreters
  • Correctness properties