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.