Generic Theorem Proving Using HOL2P: A Category Theory Inspired Approach

Abstract Integrating formal program verification into mainstream software development has proven to be quite challenging, due to the level of abstract mathematical machinery needed. Although there have been some successes, most existing methods do not adequately support the mechanical verification of generic programs. This thesis seeks to fill this gap by presenting a formalisation and implementation of a category theory inspired approach to generic program specification. Theorems to simplify verification of generic programs are developed along with a formal framework for reasoning. The result is theorem proving support based on type quantification and type operator variables in HOL, HOL2P. This is demonstrated by the verification the Yoenda Lemma.