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