Trustworthy Systems

A mechanised semantics for HOL with ad-hoc overloading

Authors

Johannes \AAman Pohjola and Arve Gengelbach

DATA61\ Uppsala University\ UNSW Sydney

Abstract

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

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

Download