This class talks about the foundations of the Isabelle/HOL proof assistant and similar proof assistants like HOL Light and HOL4, focusing on ephemeral proof objects (here described as the LCF architecture) and the underlying logic (HOL, a classical higher order logic based on the simply typed predicate calculus). There are three optional readings for the day: a blog post by Larry Paulson about the LCF architecture, a classic paper about LCF, and a later paper by Mike Gordon about the history of HOL and how it was derived from LCF.
This is the first of two classes exploring the foundations of some particular proof assistants. It looks at Isabelle/HOL, a popular proof assistant with ephemeral proof objects based on HOL. Isabelle itself is a system with a metalogic (logic for encoding logics) that supports reasoning in different logics; Isabelle/HOL instiatates this to HOL in particular.
Isabelle/HOL like other HOL variants (HOL Light and HOL4, for example) follows in the footsteps of LCF, a very early proof assistant. It keeps fairly closely to the original architecture of LCF. In the blog post, Larry describes the LCF architecture as a sort of alternative approach to the de Bruijn criterion when it comes to ensuring that proofs are correct, but I always view this as an alternative way of satisfying de Bruijn, where proofs can be reconstructed and checked, but where this is not necessary to do for correctness. We will cover this in class.