This UNSW course is about
mechanical proof assistants, how they work, and what they can be used
for. It is taught by members of the
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.
slides [pdf], slides with animations [pdf], intro demo [thy], lambda calculs demo [thy]
slides [pdf], slides with animations [pdf], HOL demo [thy] automation demo [thy] exercise template [thy]
slides [pdf], slides with animations [pdf], introductory demo [thy] simp demo [thy]
slides [pdf], slides with animations [pdf], demo [thy] - Note, there was only one lecture in Week 4 due to the public holiday.
slides [pdf], slides with animations [pdf], demo [thy], demo solution [thy] - Note, we started covering this content in Week 4.
slides [pdf], slides with animations [pdf], demo [thy], demo solution [thy], regex demo prompts [thy], regex demo solution [thy] - Note, we started covering this content in Week 5's Monday lecture.
slides [pdf], slides with animations [pdf], demo [thy], exercise template [thy], exercise solution [thy]
slides [pdf], slides with animations [pdf], auto demo [thy], Isar demo (part 1) [thy] Isar demo (part 2) [thy]
slides [pdf], slides with animations [pdf], demo [thy], demo solutions[thy]
submit using give:
give cs4161 a1 a1.thy
You can also use the web interface.
You may collect your marked assignment. Run (on a CSE machine):
~cs4161/bin/classrun -collect a1
or use the web interface.
submit using give:
give cs4161 a2 a2.thy
You can also use the web interface.
To be announced
The exam is a 24h take-home exam.
We are using this Discourse forum for class discussions. Please post questions about lecture material, the assignments and so forth on the forum.
Consults by appointment.