Generic proofs for combinator-based generic programs

12 years 7 months ago
Generic proofs for combinator-based generic programs
Abstract: 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.
Fermín Reig
Added 31 Oct 2010
Updated 31 Oct 2010
Type Conference
Year 2004
Where SFP
Authors Fermín Reig
Comments (0)