Skip to main content

A mechanised semantics for HOL with ad-hoc overloading


Johannes Åman Pohjola and Arve Gengelbach


Uppsala University

UNSW Sydney


Isabelle/HOL augments classical higher-order logic with ad-hoc overloading of constant definitions—that is, one constant may have several definitions for non-overlapping types. In this paper, we present a mechanised proof that HOL with ad-hoc overloading is consistent. All our results have been formalised in the HOL4 theorem prover.

BibTeX Entry

    issn             = {23987340},
    author           = {{\AA}man Pohjola, Johannes and Gengelbach, Arve},
    month            = may,
    date             = {2020-5-27},
    doi              = {},
    year             = {2020},
    address          = {Alicante, Spain},
    keywords         = {Interactive theorem proving; Higher-order logic; Ad-hoc overloading},
    title            = {{A} Mechanised Semantics for {HOL} with Ad-hoc Overloading},
    pages            = {498-515},
    booktitle        = {LPAR23: 23rd International Conference on Logic for Programming, Artificial Intelligence and
    volume           = {73},
    paperurl         = {},
    publisher        = {EasyChair Publications}


Served by Apache on Linux on seL4.