Appears in Science of Computer Programming, Volume 26, Number 1-3.
1996.
Pages 33–57.

PVS is a highly automated framework for specification and verification. We show how the language and deduction features of PVS can be used to formalize, mechanze, and apply some useful program transformation techniques. We examine two such examples in detail. The first is a fusion theorem due to Bird where the coposition of a catamorphism (a recursive operation on the structure of a datatype) and an anamorphism (an operation that constructs instances of the datatype) is fused to eliminate the intermediate data structure. The second example is Wand's continuation-based transformation technique for deriving tail-recursive functions from non-tail-recursive ones. These examples illustrate the utility of the language and inference features of PVS in capturing these transformations in a simple, general, and useful form.

@article{Shankar:SCP96,
    AUTHOR = {{N.} Shankar},
    TITLE = {Steps Towards Mechanizing Program Transformations Using {PVS}},
    JOURNAL = {Science of Computer Programming},
    VOLUME = {26},
    NUMBER = {1--3},
    YEAR = {1996},
    PAGES = {33--57},
    URL = {http://www.csl.sri.com/papers/scp95/}
}

• scp95.dvi.gz
• scp95.pdf
• scp95.ps