A Mechanised Semantics for HOL with Ad-hoc Overloading
Logic in Computer Science
2020-05-29 v2
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.
Keywords
Cite
@article{arxiv.2002.10212,
title = {A Mechanised Semantics for HOL with Ad-hoc Overloading},
author = {Johannes Åman Pohjola and Arve Gengelbach},
journal= {arXiv preprint arXiv:2002.10212},
year = {2020}
}
Comments
19 pages, accepted at LPAR 2020