Generic proofs for combinator-based generic programs

Fermin Reig

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


Generic programming can bring important benefits to software engineering. In particular, it reduces the burden of verification, since generic proofs can be instantiated at many types. Reasoning about programs that use type classes does not enjoy the benefits of generic reasoning, as it requires providing proofs for an arbitrary number of type instances. This makes the process very impractical. We describe a useful method to reason about a class of programs that use type classes, based on the idea that generic functions implemented using overloading can also be expressed polytypically. We demonstrate the method on functions from the scrap-your-boilerplate’ library, a collection of combinators for generic programming that has been proposed and implemented recently.

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