Alexander, PerryAustin, Evan Christopher2016-01-012016-01-012015-05-312015http://dissertations.umi.com/ku:14096https://hdl.handle.net/1808/19419Property-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.171 pagesenCopyright held by the author.Computer scienceFormal MethodsFunctional ProgrammingHaskellHaskHOLHigher-Order LogicTheorem ProvingDissertationopenAccess