Abstract. Exceptions are an indispensable part of modern programming languages. They are, however, handled poorly, especially by higherorder languages such as Standard ML and Haske...
We show how extensible records with structural subtyping can be represented directly in Higher-Order Logic (HOL). Exploiting some specific properties of HOL, this encoding turns o...