Teaching Higher-Order Logic Using Isabelle
This work addresses the challenge of making higher-order logic more approachable for learners, though it is incremental as it builds on existing proof assistant frameworks.
The authors tackled the problem of teaching higher-order logic by developing a formalization in Isabelle that is small and readable, aiming to provide an accessible introduction without the complexity of existing systems like Isabelle/HOL.
We present a formalization of higher-order logic in the Isabelle proof assistant, building directly on the foundational framework Isabelle/Pure and developed to be as small and readable as possible. It should therefore serve as a good introduction for someone looking into learning about higher-order logic and proof assistants, without having to study the much more complex Isabelle/HOL with heavier automation. To showcase our development and approach we explain a sample proof, describe the axioms and rules of our higher-order logic, and discuss our experience with teaching the subject in a classroom setting.