Program synthesis via extraction of programs from constructive proofs is now very well established, with a large literature base. There are still quite a few hurdles to overcome, but the meta-theory has been in place for quite some time now.
It is thus disappointing that the authors of the paper seem to ignore almost all of it. Looking at their references, one is at once struck by how old most of them are; this is not necessarily bad--the pioneers deserve continued recognition. But this research area is currently extremely active, so it is baffling to find no reference to it at all. Especially since there really is a lot of relevant work around; various items done with Coq [1], Isabelle [2], or ACL2 [3] come immediately to mind. Every proof strategy that I looked up was known or a special case of a strategy in Visser’s 2005 survey [4]. Automating such proofs is now considered feasible; see Claesen and colleagues [5] for just one example.
Digging a little deeper, it is surprising that there are also no real references for the theory of lists; in particular, Bird’s classic paper [6] (cited 524 times, thus rather well known) is apparently unknown to the authors. It should also be noted that the authors reference 11 of their own papers, five of which are actually technical reports.
Fundamentally, this work is very ad hoc and ignores most of the current research on the topic. It is also made extra hard to read by using non-standard notation throughout.