#### HOLCF '11: A Definitional Domain Theory for Verifying Functional Programs

#### Brian Huffman

HOLCF is an interactive theorem proving system that uses the mathematics of domain theory to reason about programs written in functional programming languages. This thesis introduces HOLCF '11, a thoroughly revised and extended version of HOLCF that advances the state of the art in program verification: HOLCF '11 can reason about many program definitions that are beyond the scope of other formal proof tools, while providing a high degree of proof automation. The soundness of the system is ensured by adhering to a definitional approach: New constants and types are defined in terms of previous concepts, without introducing new axioms.

Major features of HOLCF '11 include two high-level definition packages: the Fixrec package for defining recursive functions, and the Domain package for defining recursive datatypes. Each of these uses the domain-theoretic concept of least fixed points to translate user-supplied recursive specifications into safe low-level definitions. Together, these tools make it easy for users to translate a wide variety of functional programs into the formalism of HOLCF. Theorems generated by the tools also make it easy for users to reason about their programs, with a very high level of confidence in the soundness of the results.

As a case study, we present a fully mechanized verification of a model of concurrency based on powerdomains. The formalization depends on many features
unique to HOLCF '11, and is the first verification of such a model in a formal
proof tool.

HOLCF '11: A Definitional Domain Theory for Verifying Functional Programs by Brian Huffman is licensed under a Creative Commons Attribution 3.0 Unported License.
pdf

BibTeX:

@phdthesis{holcf11,
author = {Brian Huffman},
title = {HOLCF '11: A Definitional Domain Theory for Verifying Functional Programs},
school = {Portland State University},
year = {2012}
}