Proof Assistants

• Assignment I: The IMP language in Isabelle
  • Handout with the tasks and details on the marking scheme.
  • Theory files (tar / zip). Please use the file Assignment1.thy as a template.

• Assignment II: Simply typed lambda calculus in Coq
  • Handout with instructions (including installation instructions) and details on the marking scheme.
  • Coq files: tar / zip.

See the syllabus for more general information about the assessment.