Abstract

The current state of the art in functional program verification uses automated proof by induction to check properties. This approach is used in the well established ACL2 for Common LISP , and the more recent HipSpec for Haskell.

This talk describes an alternative approach where terms within properties are simplified until the property becomes trivially true. The simplification technique we use is called “fixpoint fusion”, but also goes by the names “deforestation” and “supercompilation”. We first present applications of this process which can verify properties at the same level as ACL2 or HipSpec. We then present an extension which allows for the fully automatic simplifications “isSorted (treesort xs) => True” and “isSorted (quicksort xs) => True”, both of which it is fundamentally impossible for ACL2 or HipSpec to solve without user provided lemmas.