Yun-Yan Chi and Shin-Cheng Mu. In the *9th Asian Symposium on Programming Languages and Systems* (APLAS 2011), LNCS 7078, pages 74-88.

[PDF]

The well-known third list homomorphism theorem states that if a function `h`

is both an instance of `foldr`

and `foldl`

, it is a list homomorphism. Plenty of previous works devoted to constructing list homomorphisms, however, overlook the fact that proving `h`

is both a `foldr`

and a `foldl`

is often the hardest part which, once done, already provides a useful hint about what the resulting list homomorphism could be. In this paper we propose a new approach: to construct a possible candidate of the associative operator and, at the same time, to transform a *proof* that `h`

is both a `foldr`

and a `foldl`

to a proof that `h`

is a list homomorphism. The effort constructing the proof is thus not wasted, and the resulting program is guaranteed to be correct.