This UNSW course is about
mechanical proof assistants, how they work, and what they can be used
for. It is taught by members of
Data61's Trustworthy Systems
group. The course presents specification and proof techniques used in
industrial grade interactive theorem provers, teaches the theoretical background
to the techniques involved, and shows how to use a theorem prover to
conduct formal proofs in practice.
Topics include higher order logic, natural deduction, lambda calculus, term rewriting, data types and recursive functions, induction principles, and proofs about programs. See the course outline for a full content overview and prerequisites.
The course will provide hands-on experience with the proof assistant Isabelle/HOL.
Slides and Isabelle files will be made available online as the lectures progress.
Setting up Isabelle, basic rules and cheat sheet.
Textbook, further reading, and links the tools used in the lecture.
Will become available here as course progresses.
demo [thy] (as developed in the lecture + bonus content)
The exam will be a 24h take-home exam. It will start Wed, 2 Dec 2020, 8am AEDT (Sydney time), and end 3 Dec 2020, 7:59am AEDT (Sydney time).
You need to submit a .thy file using give:
give cs4161 exam exam.thy
You can also use the web interface.
If you have trouble using the submission system, you can also submit your exam to one of the lecturers by email.