@unpublished(spc002,
 author       = {Rob Arthan},
 title        = {{HOL} Formalised: Semantics},
 url          = {http://www.lemma-one.com/ProofPower/specs/spc002.pdf},
)
@inproceedings(Art14,
 author       = {Rob Arthan},
 year         = {2014},
 title        = {{{HOL Constant Definition Done Right}}},
 booktitle    = {Interactive {{Theorem Proving}}},
 publisher    = {{Springer International Publishing}},
 pages        = {531--536},
 doi          = {10.1007/978-3-319-08970-6_34},
)
@unpublished(farmer94,
 author       = {William~M. Farmer},
 title        = {A General Method for Safely Overwriting Theories in Mechanized Mathematics Systems},
 url          = {http://imps.mcmaster.ca/doc/overwriting-theories.pdf},
)
@inproceedings(DBLP:journals/entcs/GengelbachW18,
 author       = {Arve Gengelbach and Tjark Weber},
 year         = {2017},
 title        = {Model-Theoretic {C}onservative {E}xtension for {D}efinitional {T}heories},
 editor       = {Sandra Alves and Renata Wasserman},
 booktitle    = {12th Workshop on Logical and Semantic Frameworks, with Applications, {LSFA} 2017, Bras{\'{\i}}lia, Brazil, September 23-24, 2017},
 series       = {Electronic Notes in Theoretical Computer Science},
 volume       = {338},
 publisher    = {Elsevier},
 pages        = {133--145},
 doi          = {10.1016/j.entcs.2018.10.009},
)
@inproceedings(GengelbachW20,
 author       = {Arve Gengelbach and Tjark Weber},
 year         = {2020},
 title        = {{Proof-theoretic Conservativity for HOL with Ad-hoc Overloading}},
 editor       = {Violet Ka~I Pun and Volker Stolz and Adenilso da~Silva~Sim{\~{a}}o},
 booktitle    = {Theoretical Aspects of Computing - {ICTAC} 2020 - 17th International Colloquium, Macau, China, November 30 - December 4, 2020, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {12545},
 publisher    = {Springer},
 pages        = {23--42},
 doi          = {10.1007/978-3-030-64276-1_2},
)
@article(DBLP:journals/jfrea/GrabowskiKN10,
 author       = {Adam Grabowski and Artur Kornilowicz and Adam Naumowicz},
 year         = {2010},
 title        = {Mizar in a Nutshell},
 journal      = {J. Formalized Reasoning},
 volume       = {3},
 number       = {2},
 pages        = {153--245},
 doi          = {10.6092/issn.1972-5787/1980},
)
@inproceedings(DBLP:conf/types/HaftmannW06,
 author       = {Florian Haftmann and Makarius Wenzel},
 year         = {2006},
 title        = {Constructive Type Classes in Isabelle},
 editor       = {Thorsten Altenkirch and Conor McBride},
 booktitle    = {Types for Proofs and Programs, International Workshop, {TYPES} 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers},
 series       = {Lecture Notes in Computer Science},
 volume       = {4502},
 publisher    = {Springer},
 pages        = {160--174},
 doi          = {10.1007/978-3-540-74464-1\_11},
)
@inproceedings(KuArMyOw14,
 author       = {Ramana Kumar and Rob Arthan and Magnus~O. Myreen and Scott Owens},
 year         = {2014},
 title        = {{{HOL}} with {{Definitions}}: {{Semantics}}, {{Soundness}}, and a {{Verified Implementation}}},
 booktitle    = {Interactive {{Theorem Proving}}},
 publisher    = {{Springer, Cham}},
 pages        = {308--324},
 doi          = {10.1007/978-3-319-08970-6_20},
)
@article(DBLP:journals/jar/KumarAMO16,
 author       = {Ramana Kumar and Rob Arthan and Magnus~O. Myreen and Scott Owens},
 year         = {2016},
 title        = {Self-Formalisation of Higher-Order Logic - Semantics, Soundness, and a Verified Implementation},
 journal      = {J. Autom. Reasoning},
 volume       = {56},
 number       = {3},
 doi          = {10.1007/s10817-015-9357-x},
)
@inproceedings(DBLP:conf/cpp/Kuncar15,
 author       = {Ondrej Kuncar},
 year         = {2015},
 title        = {Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading in Proof Assistants},
 editor       = {Xavier Leroy and Alwen Tiu},
 booktitle    = {Proceedings of the 2015 Conference on Certified Programs and Proofs, {CPP} 2015, Mumbai, India, January 15-17, 2015},
 publisher    = {{ACM}},
 pages        = {85--94},
 doi          = {10.1145/2676724.2693175},
)
@article(DBLP:journals/pacmpl/Kuncar018,
 author       = {Ondrej Kuncar and Andrei Popescu},
 year         = {2018},
 title        = {Safety and conservativity of definitions in {HOL} and Isabelle/HOL},
 journal      = {{PACMPL}},
 volume       = {2},
 number       = {{POPL}},
 pages        = {24:1--24:26},
 doi          = {10.1145/3158112},
)
@article(DBLP:journals/jar/KuncarP19a,
 author       = {Ondrej Kuncar and Andrei Popescu},
 year         = {2019},
 title        = {A Consistent Foundation for Isabelle/HOL},
 journal      = {J. Autom. Reasoning},
 volume       = {62},
 number       = {4},
 pages        = {531--555},
 doi          = {10.1007/s10817-018-9454-8},
)
@inproceedings(KuncarPopescu2017a,
 author       = {Kun\IeC{\v c}ar, Ond\IeC{\v r}ej and Andrei Popescu},
 year         = {2017},
 title        = {Comprehending {{Isabelle}}/{{HOL}}'s {{Consistency}}},
 editor       = {Hongseok Yang},
 booktitle    = {Programming {{Languages}} and {{Systems}} - 26th {{European Symposium}} on {{Programming}}, {{ESOP}} 2017, {{Held}} as {{Part}} of the {{European Joint Conferences}} on {{Theory}} and {{Practice}} of {{Software}}, {{ETAPS}} 2017, {{Uppsala}}, {{Sweden}}, {{April}} 22-29, 2017, {{Proceedings}}},
 series       = {Lecture Notes in Computer Science},
 volume       = {10201},
 publisher    = {{Springer}},
 pages        = {724--749},
 doi          = {10.1007/978-3-662-54434-1_27},
)
@misc(HOL14,
 author       = {Michael Norrish and Konrad Slind},
 year         = {2014},
 title        = {The {{HOL System LOGIC}}},
 url          = {http://downloads.sourceforge.net/project/hol/hol/kananaskis-10/kananaskis-10-logic.pdf},
)
@inproceedings(DBLP:conf/rta/Obua06,
 author       = {Steven Obua},
 year         = {2006},
 title        = {Checking Conservativity of Overloaded Definitions in Higher-Order Logic},
 editor       = {Frank Pfenning},
 booktitle    = {Term Rewriting and Applications, 17th International Conference, {RTA} 2006, Seattle, WA, USA, August 12-14, 2006, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {4098},
 publisher    = {Springer},
 pages        = {212--226},
 doi          = {10.1007/11805618\_16},
)
@incollection(pitts1993,
 author       = {Andrew~M. Pitts},
 year         = {1993},
 title        = {The {HOL} Logic},
 editor       = {M.J.C. Gordon and Tom Melham},
 booktitle    = {Introduction to {HOL}: A Theorem-Proving Environment for Higher-Order Logic},
 publisher    = {Cambridge University Press},
 pages        = {191--232},
)
@inproceedings(LPAR23:AmPoGen20,
 author       = {Johannes~{\r A}man Pohjola and Arve Gengelbach},
 year         = {2020},
 title        = {A Mechanised Semantics for HOL with Ad-hoc Overloading},
 editor       = {Elvira Albert and Laura Kov{\'{a}}cs},
 booktitle    = {LPAR23. LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
 series       = {EPiC Series in Computing},
 volume       = {73},
 publisher    = {EasyChair},
 pages        = {498--515},
 doi          = {10.29007/413d},
 url          = {https://easychair.org/publications/paper/9Hcd},
)
@inproceedings(Rudnicki92,
 author       = {Piotr Rudnicki},
 year         = {1992},
 title        = {An Overview of the Mizar Project},
 editor       = {Nordstr\IeC{\"o}m, Bengt and Kent Petersson and Gordon Plotkin},
 booktitle    = {Proceedings of the 1992 Workshop on Types for Proofs and Programs},
 pages        = {311--332},
 url          = {http://mizar.org/project/MizarOverview.pdf},
)
@book(Sho67,
 author       = {Joseph~R. Shoenfield},
 year         = {1967},
 title        = {Mathematical {{Logic}}},
 publisher    = {{A.K. Peters}},
 address      = {Natick, Mass},
)
@inproceedings(DBLP:conf/tphol/Wenzel97,
 author       = {Markus Wenzel},
 year         = {1997},
 title        = {Type Classes and Overloading in Higher-Order Logic},
 editor       = {Elsa~L. Gunter and Amy~P. Felty},
 booktitle    = {Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {1275},
 publisher    = {Springer},
 pages        = {307--322},
 doi          = {10.1007/BFb0028402},
)