Midterm Exam

Midterm

Available: March 28 at 2:30

Due: March 29 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.

Dowload: Midterm Exam

Source: LaTeX

Topics:

• Specification
  • Inductive types
  • Non-recursive definitions
  • Fixpoint definitions
  • Theorems
  • Type variables and polymorphisms
  • Logic
• Constructive specification
  • Defining constructors
  • Defining properties over constructors
  • Defining correctness theorems
• Proof tactics
  • intros - instaintiating 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