Please use this identifier to cite or link to this item:
http://hdl.handle.net/11375/21329
Full metadata record
DC Field | Value | Language |
---|---|---|
dc.contributor.advisor | Kahl, Wolfram | - |
dc.contributor.author | Wang, Feng | - |
dc.date.accessioned | 2017-05-02T16:08:48Z | - |
dc.date.available | 2017-05-02T16:08:48Z | - |
dc.date.issued | 2007-09 | - |
dc.identifier.uri | http://hdl.handle.net/11375/21329 | - |
dc.description.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> | en_US |
dc.language.iso | en_US | en_US |
dc.subject | verification, Haskell type classes, programming language, QuickCheck, functions | en_US |
dc.title | Verification of Haskell Type Classes | en_US |
dc.type | Thesis | en_US |
dc.contributor.department | Computing and Software | en_US |
dc.description.degreetype | Thesis | en_US |
dc.description.degree | Master of Applied Science (MASc) | en_US |
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.