A Mechanised Semantics for HOL with Ad-hoc Overloading

02/24/2020
by   Johannes Åman Pohjola, et al.
0

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.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset