Name
Abstract | ||
|---|---|---|
We present a proof rule and an effective tactic for proving properties about Haskell type classes by proving them for the available instance definitions. This is not straightforward, because instance definitions may depend on each other. The proof assistant Isabelle handles this problem for single parameter type classes by structural induction on types. However, this does not suffice for an effective tactic for more complex forms of overloading. We solve this using an induction scheme derived from the instance definitions. The tactic based on this rule is implemented in the proof assistant Sparkle. |
Year | Venue | Keywords |
|---|---|---|
2004 | Trends In Functional Programming | theorem proving,functional programming,type classes |
DocType | Citations | PageRank |
Conference | 5 | 0.44 |
References | Authors | |
6 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ron Van Kesteren | 1 | 45 | 2.46 |
| marko c j d van eekelen | 2 | 239 | 30.37 |
| Maarten de Mol | 3 | 119 | 8.29 |