Teaching Higher-Order Logic Using Isabelle
<|reference_start|>Teaching Higher-Order Logic Using Isabelle: 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.<|reference_end|>
@article{lund2024teaching,
    title={Teaching Higher-Order Logic Using Isabelle},
    author={Simon Tobias Lund (Technical University of Denmark), J{o}rgen
  Villadsen (Technical University of Denmark)},
    journal={EPTCS 400, 2024, pp. 59-78},
    year={2024},
    doi={10.4204/EPTCS.400.5},
    archivePrefix={arXiv},
    eprint={2404.05458},
    primaryClass={cs.LO cs.AI}
}