Report Number: CS-TR-75-520
Institution: Stanford University, Department of Computer Science
Title: On the representation of data structures in LCF with applications to program generation.
Author: von Henke, Friedrich W.
Date: September 1975
Abstract: In this paper we discuss techniques of exploiting the obvious relationship between program structure and data structure for program generation. We develop methods of program specification that are derived from a representation of recursive data structures in the Logic for Computable Functions (LCF). As a step towards a formal problem specification language we define definitional extensions of LCF. These include a calculus for (computable) homogeneous sets and restricted quantification. Concepts that are obtained by interpreting data types as algebras are used to derive function definition schemes from an LCF term representing a data structure; they also lead to techniques for the simplification of expressions in the extended language. The specification methods are illustrated with a detailed example.
http://i.stanford.edu/pub/cstr/reports/cs/tr/75/520/CS-TR-75-520.pdf