Assignments

There will be three written assignments during the course. Some of these will involve proofs in the Isabelle theorem prover. They will be made available from this page as the course progresses.

  • Assignment 1: assignment [pdf], Isabelle template [thy]

    Submit using give on a CSE machine:

    give cs4161 a1 files

    You need to submit a .thy file, along with a .txt file or a .pdf file, for example

    give cs4161 a1 a1.thy a1.pdf

    or

    give cs4161 a1 a1.thy a1.txt -->

  • Solution to assignment 1: Text questions [pdf], Isabelle proofs [thy]
  • Assignment 2: assignment [pdf], Isabelle template [thy]
  • Solution to assignment 2: Isabelle proofs [thy]
  • Assignment 3: assignment [pdf], Isabelle template [thy]
  • Solution to assignment 3: Isabelle proofs [thy]
  • You may collect your marked assignments. Run (on a CSE machine):

    ~cs4161/bin/classrun -collect a3