{"id":{"repo_id":"essex","oai_identifier":"oai:repository.essex.ac.uk:20690"},"canonical_url":"https://search.dev.ndltd.org/etd/essex/oai:repository.essex.ac.uk:20690","repository":{"repo_id":"essex","name":"University of Essex","base_url":"https://repository.essex.ac.uk/cgi/oai2"},"display":{"title":"Generic Theorem Proving Using HOL2P: A Category Theory Inspired Approach","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Harriott, Keisha"],"institution":"University of Essex","degree_name":null,"degree_level":"masters","degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2014,"date_issued":"2014-02","date_published":"2014-02","updated_at":"2026-07-24T02:18:18Z","subjects":["QA75 Electronic computers. Computer science"],"languages":["en"],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":null,"outbound_label":null,"outbound_source":null},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:creator","label":"Author","values":["Harriott, Keisha"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2014-02-11"]},{"key":"dc:date.issued","label":"Date","values":["2014-02"]},{"key":"dc:publisher.department","label":"Dc Publisher Department","values":["School of Computer Science and Electronic Engineering"]},{"key":"dc:publisher.institution","label":"Dc Publisher Institution","values":["University of Essex"]},{"key":"dc:relation.isreferencedby","label":"Dc Relation Isreferencedby","values":["https://repository.essex.ac.uk/20690/"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"dc:type.qualificationlevel","label":"Dc Type Qualificationlevel","values":["masters"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["QA75 Electronic computers. Computer science"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://repository.essex.ac.uk/20690/1/Thesis_vr1.pdf"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:format","label":"Dc Format","values":["text"]},{"key":"dc:title","label":"Title","values":["Generic Theorem Proving Using HOL2P: A Category Theory Inspired Approach"]}]}],"canonical_facts":{"dc:creator":["Harriott, Keisha"],"dc:date":["2014-02-11"],"dc:date.issued":["2014-02"],"dc:description.abstract":["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."],"dc:format":["text"],"dc:identifier.uri":["https://repository.essex.ac.uk/20690/1/Thesis_vr1.pdf"],"dc:language":["en"],"dc:publisher.department":["School of Computer Science and Electronic Engineering"],"dc:publisher.institution":["University of Essex"],"dc:relation.isreferencedby":["https://repository.essex.ac.uk/20690/"],"dc:subject":["QA75 Electronic computers. Computer science"],"dc:title":["Generic Theorem Proving Using HOL2P: A Category Theory Inspired Approach"],"dc:type":["Thesis"],"dc:type.qualificationlevel":["masters"]},"updated_at":"2026-07-24T02:18:18Z"}