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.
  • Please submit your work via Moodle by the due date of 16 November 2026, 12 noon.
  • Reminder: You must work on the assignment as an individual, and the use of AI (other than the Sledgehammer tool built into Isabelle) is not permitted for writing the formalisation, proofs, or reports.

See the syllabus for more general information about the assessment.