NICTA Advanced Course
Theorem Proving - Principles, Techniques, Applications
This is an advanced NICTA course aimed at
fourth year and postgraduate students. It is provided at UNSW, ANU,
and University of Melbourne across a video link from the NICTA Formal
Methods program based at UNSW/Sydney.
There is no formal enrollment at ANU, UNSW, or Melbourne
necessary. Please send an email to Gerwin Klein
<gerwin.klein@nicta.com.au> if you would like to be included in
the lecture mailing list. The course is free, there will be no
assignments, but also no credits.
Presenter: Gerwin Klein (NICTA/Formal Methods)
Description:
This 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 backround 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,
and proofs about programs.
Locations:
- Sydney: Room G3 in the UNSW Electrical Engineering Building (G17)
- Canberra: NICTA board room (216 Northbourne Ave, Braddon)
- Melbourne: to be announced
Session times:
- Wed 4th August 2004 till Mon 20 September 2004
- Mon, 14:00h - 15:30h
- Wed, 10:30h - 12:00h
- Exceptions: Mon 6.9., 13.9., 20.9. are 15:00h - 16:30h
Workload:
- presentation time: 3h/week
- extra reading: 1h/week
- assignments: 3h/week (voluntary exercises)
More information and lecture slides will be made available on this page during the course.
Slides:
- Lecture 1:
slides [pdf, online]
slides [pdf, printable]
demo [thy]
- Lecture 2:
slides [pdf, online]
slides [pdf, printable]
demo [thy]
- Lecture 3:
slides [pdf, online]
slides [pdf, printable]
demo [thy]
- Lecture 4:
slides [pdf, online]
slides [pdf, printable]
demo [thy]
exercises [thy]
- Lecture 5:
slides [pdf, online]
slides [pdf, printable]
demo [thy]
demo 2 [thy]
- Lecture 6:
slides [pdf, online]
slides [pdf, printable]
demo [thy]
- Lecture 7:
slides [pdf, online]
slides [pdf, printable]
demo [thy]
- Lecture 8:
slides [pdf, online]
slides [pdf, printable]
demo [thy]
- Lecture 9:
slides [pdf, online]
slides [pdf, printable]
demo [thy]
- Lecture 10:
slides [pdf, online]
[or_commute.v]
[tree.v]
[coins.v]
[mod2.v]
[dep.v]
(guest lecture by Nicolas Magaud)
- Lecture 11:
slides [pdf, online]
(guest lecture by Michael Norrish)
- Lecture 12:
slides [pdf, online]
slides [pdf, printable]
demo [thy]
- Lecture 13:
slides [pdf, online]
slides [pdf, printable]
demo [thy]
demo [thy]
hoare logic setup [thy]
- Lecture 14:
slides [pdf, online]
slides [pdf, printable]
demo [thy]
demo batch session [tar.gz]
proof document [pdf]
Further Reading:
- Tobias Nipkow, Lawrence C. Paulson,
Markus Wenzel: Isabelle/HOL - A
Proof Assistant for Higher-Order Logic, LNCS 2283,
Springer, 2002.
This is the official Isabelle tutorial. Easy to read, with lots of exercises.
-
Isabelle system and reference documentation.
If you need to know something about Isabelle in gory detail.
- Hendrik Pieter Barendregt. The Lambda Calculus,
its Syntax and Semantics, North-Holland, 2nd edition, 1984.
- Chris Hankin. Lambda Calculi. A Guide for
Computer Scientists, Ofxord University Press, 1994.
- Tobias Nipkow,
Functional Unification of Higher-Order Patterns,
In: Proc. 8th IEEE Symp. Logic in Computer Science, p. 64-74, 1993.
- Wolfgang Naraschewski and Tobias Nipkow,
Type Inference Verified: Algorithm W in Isabelle/HOL,
Journal of Automated Reasoning, volume 23, p. 299-318, 1999.
- Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56 68, 1940.
- Michael J. C. Gordon and Tom F. Melham (eds), Introduction to HOL. Cambridge University Press, 1993.
- Jeremy Avigad and Richard Zach,
The Epsilon Calculus,
The Stanford Encyclopedia of Philosophy (Summer 2002 Edition), Edward N. Zalta (ed.), 2002.
- Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
- Jeremy Avigad. Mathematical method and proof. 2004.
- Elsa L. Gunter. Why
we can't have SML style datatype declarations in HOL. In
L. J. M. Claese and M. J. C. Gordon, editors, Higher Order Logic
Theorem Proving and Its Applications, volume A-20 of IFIP
Transactions, pages 561-568. North-Holland Press, September 1992.
- Stefan Berghofer and Markus Wenzel. Inductive
datatypes in HOL - lessons learned in Formal-Logic Engineering. In
Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, L. Théry, editors,
TPHOLs'99, LNCS 1690. Springer-Verlag 1999.
- John Harrison. Inductive
definitions: automation and application. Proceedings of the 1995
International Workshop on Higher Order Logic theorem proving and its
applications, Aspen Grove, Utah, 1995. Springer LNCS 971, pp. 200-213,
1995.
- Hanne Riis Nielson, Flemming Nielson.
Semantics with Applications: A Formal Introduction. 1999.
Links: