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.

Creative Commons License
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}
}