Back to Search
Start Over
A Mechanised Semantics for HOL with Ad-hoc Overloading
- Publication Year :
- 2020
-
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.
Details
- Database :
- OAIster
- Notes :
- English
- Publication Type :
- Electronic Resource
- Accession number :
- edsoai.on1235269220
- Document Type :
- Electronic Resource
- Full Text :
- https://doi.org/10.29007.413d