Please use this identifier to cite or link to this item:
http://hdl.handle.net/11375/21329
Title: | Verification of Haskell Type Classes |
Authors: | Wang, Feng |
Advisor: | Kahl, Wolfram |
Department: | Computing and Software |
Keywords: | verification, Haskell type classes, programming language, QuickCheck, functions |
Publication Date: | Sep-2007 |
Abstract: | <p> The Haskell programming language uses type classes to deal with overloading. Functions are overloaded by defining some types to be instances of a class. A meaningful instance should satisfy the invariants of the class.</p> <p> In this thesis we present one method to validate the type instances of classes informally, and another one to verify them in a formal way.</p> <p> The first method uses QuickCheck, which is an automatic testing tool for Haskell programs. We introduce how to specify the properties of type classes in QuickCheck by some examples, and I also present testing for Haskell standard types and classes.</p> <p> The second method I adopted uses the theorem prover Isabelle/HOL. To facilitate the usage of Isabelle/HOL for Haskell programmers, I define a set of translation rules from Haskell programs to Isabelle/HOL, and design a simple automatic translating tool based on those rules. Logical differences between Haskell and Isabelle/HOL need to be considered in the translation. For example Isabelle/HOL is not suitable to describe the semantics of lazy evaluation and of Haskell functions that are non-terminating. I also prove some type instances to illustrate how the properties are verified in Isabelle/HOL.</p> |
URI: | http://hdl.handle.net/11375/21329 |
Appears in Collections: | Digitized Open Access Dissertations and Theses |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
Wang_Feng_2007Sept_Masters..pdf | 2.56 MB | Adobe PDF | View/Open |
Items in MacSphere are protected by copyright, with all rights reserved, unless otherwise indicated.