Loading...
Theorem Provers as Libraries -- An Approach to Formally Verifying Functional Programs
Austin, Evan Christopher
Austin, Evan Christopher
Citations
Altmetric:
Abstract
Property-directed verification of functional programs tends to take one of two paths. First, is the traditional testing approach, where properties are expressed in the original programming language and checked with a collection of test data. Alternatively, for those desiring a more rigorous approach, properties can be written and checked with a formal tool; typically, an external proof system. This dissertation details a hybrid approach that captures the best of both worlds: the formality of a proof system paired with the native integration of an embedded, domain specific language (EDSL) for testing. At the heart of this hybridization is the titular concept -- a theorem prover as a library. The verification capabilities of this prover, HaskHOL, are introduced to a Haskell development environment as a GHC compiler plugin. Operating at the compiler level provides for a comparatively simpler integration and allows verification to co-exist with the numerous other passes that stand between source code and program.
Description
Date
2015-05-31
Journal Title
Journal ISSN
Volume Title
Publisher
University of Kansas
Files
Research Projects
Organizational Units
Journal Issue
Keywords
Computer science, Formal Methods, Functional Programming, Haskell, HaskHOL, Higher-Order Logic, Theorem Proving