NAME
	Sara Kalvala and Mike Squire
TITLE
	An introduction to interactive theorem proving
TYPE
	Introductory
SECTION
	Computation and Logic
DURATION
	1 week
SUMMARY

Research in logic and its applications can benefit from tools that
allow mechanical manipulation of logical formulae. By incorporating
rules of logical systems into a software system, one can check the
match between a formal system and desired properties, investigate
correctness aspects, develop proof techniques, and perform large
proofs with a fair degree of accuracy

This advanced hands-on course will concentrate on teaching Isabelle, a
proof environment that can help researchers in two ways: it is an
advanced theorem prover for Higher Order Logic and ZF Set Theory, and
both these logics are well known for providing a powerful formalism
for proofs. Isabelle is also a system for embedding different logics
through the inbuilt meta-logic, and this allows users to build a rapid
prototype of a prover for novel logical systems.

Participants will first learn how to perform proofs in Higher Oder
Logic, exploring both the interactive environment and existing proof
strategies in Isabelle. They will then have a chance to explore the
meta-logic and learn how different object logics are written into
Isabelle and how proof strategies for such new logics can be
programmed. Finally, some other systems that satisfy the above two
roles (such as Coq, PVS, and HOL) will be examined briefly.