Title: Introduction to Isabelle/HOL

Abstract: 
Higher-order logic is a very expressive formalism which has been used to reason about various domains, such as software, hardware, and various other areas of pure and applied mathematics. Isabelle/HOL is a program which facilitates formalisation in higher-order logic, and it provides various features that support formalisation and reasoning. Compared to similar systems it offers a very attractive combination of usability, safety and automation. This tutorial is intended to introduce you to Isabelle/HOL by demonstrating its use, giving examples of what Isabelle/HOL has been used for, and explaining some of the background theory. 

This is intended to be a "hands on" tutorial, and arrangements are being made to have all the required software installed on lab machines for you to play with. In order to make the most out of this tutorial, it would be very useful for attendees to be familiar with undergraduate logic and functional programming.