Model-Theoretic Conservative Extension for Definitional Theories. - Arve Gengelbach; Tjark Weber (LSFA, 2017)

Proof-Theoretic Conservative Extension of HOL with Ad-hoc Overloading. - Arve Gengelbach; Tjark Weber (ICTAC, 2020)

A Mechanised Semantics for HOL with Ad-hoc Overloading. - Johannes Åman Pohjola; Arve Gengelbach (LPAR, 2020)

Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading. - Arve Gengelbach; Johannes Åman Pohjola; Tjark Weber (LFMTP, 2020)

Conservative Definitions for Higher-order Logic with Ad-hoc Overloading. - Arve Gengelbach (2021)

A Verified Cyclicity Checker: For Theories with Overloaded Constants. - Arve Gengelbach; Johannes Åman Pohjola (ITP, 2022)