Theorem Provers as Libraries -- An Approach to Formally Verifying Functional Programs
Issue Date
2015-05-31Author
Austin, Evan Christopher
Publisher
University of Kansas
Format
171 pages
Type
Dissertation
Degree Level
Ph.D.
Discipline
Electrical Engineering & Computer Science
Rights
Copyright held by the author.
Metadata
Show full item recordAbstract
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.
Collections
- Dissertations [4700]
- Engineering Dissertations and Theses [1055]
Items in KU ScholarWorks are protected by copyright, with all rights reserved, unless otherwise indicated.
We want to hear from you! Please share your stories about how Open Access to this item benefits YOU.