Interactive Theorem Proving - Principles, Techniques, Applications


  Data61       CSIRO
COMP4161 is a 6 UoC advanced Data61 course at CSE/UNSW aimed at fourth year and postgraduate students. Third and second year students with permission of lecturer are welcome.

The course is about mechanical proof assistants, how they work, and what they can be used for. It presents specification and proof techniques used in industrial grade theorem provers, teaches the theoretical background to the techniques involved, and shows how to use a theorem prover to conduct formal proofs in practice. The course is intended to bring fourth year and postgraduate students into contact with current research topics in the field of theorem proving and automated deduction and to teach them the necessary skills to successfully use industrial grade verification environments in modelling and verification.

Topics include higher order logic, natural deduction, lambda calculus, term rewriting, data types and recursive functions, induction principles, calculational reasoning, mathematical proofs, decision procedures for a variety of logical domains, and proofs about programs.

The course will provide hands-on experience with the proof assistant Isabelle/HOL.

48 UoC. Familiarity with functional programming and mathematical logic is required.

Session times:
  • Mon, 10:00h - 11:30h (Colombo LG02; K-B16-LG02)
  • Thu, 9:00h - 10:30h (Webster 256; K-G14-256)
  • Lectures are running weeks 1-12
  • Exam on 14 Nov