On the Representation of Data Structures in LCF with Applications to Program Generation
Abstract
In this paper techniques of exploiting the obvious relationship between program structure and data structure for program generation are discussed. Methods of program specification are developed 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 a 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. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 01, 1975
- Accession Number
- ADA019664
Entities
People
- Frederich W. Von Henke
Organizations
- Stanford University