Treating Partiality in a Logic of Total Functions

The need to use partial functions arises frequently in formal descriptions of computer systems. However, most proof assistants are based on logics of total functions. To address this mismatch, various approaches to partiality have been developed, new logical solutions as well as practical workarounds. In this paper we survey and compare methods used to support partiality in a mechanization of a higher order logic featuring only total functions. The techniques we survey and compare are generally applicable and are illustrated by relatively large examples.

paper