Proof Support for General Type Classes

Ron van Kesteren, Marko van Eekelen, Maarten de Mol

To appear at Symposium on Trends in Functional Programming (TFP04), Munich, Germany, 25-26 November, 2004


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.

Server START Conference Manager
Update Time 11 Mar 2005 at 20:15:19
Start Conference Manager
Conference Systems