Research Repository

Generic Theorem Proving Using HOL2P: A Category Theory Inspired Approach

Harriott, Keisha (2014) Generic Theorem Proving Using HOL2P: A Category Theory Inspired Approach. Masters thesis, University of Essex.


Download (484kB) | Preview


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.

Item Type: Thesis (Masters)
Subjects: Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Divisions: Faculty of Science and Health > Computer Science and Electronic Engineering, School of
Depositing User: Keisha Harriott
Date Deposited: 21 Nov 2017 14:45
Last Modified: 21 Nov 2017 14:47

Actions (login required)

View Item View Item