The University of New South Wales

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

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