Dissertation/Thesis Abstract

Theorem Provers as Libraries - An Approach to Formally Verifying Functional Programs
by Austin, Evan, Ph.D., University of Kansas, 2015, 171; 3706073
Abstract (Summary)

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.

Indexing (document details)
Advisor: Alexander, Perry
Commitee: Agah, Arvin, Gill, Andy, Kulkarni, Prasad, Van Vleck, Erik
School: University of Kansas
Department: Electrical Engineering and Computer Science
School Location: United States -- Kansas
Source: DAI-B 76/10(E), Dissertation Abstracts International
Subjects: Computer science
Keywords: Formal methods, Functional programming, Haskell, Haskhol, Higher-order logic, Theorem proving
Publication Number: 3706073
ISBN: 978-1-321-79519-6
Copyright © 2020 ProQuest LLC. All rights reserved. Terms and Conditions Privacy Policy Cookie Policy