Specification of data structures for FP programs
Geoffrey A. Frank · 1981
An essential part of an FP programmer's task is keeping track of the intermediate data structures of an FP program. This paper describes a way of documenting FP program with descriptions of its data structures and automatically proving that this documentation is accurate.