Jensen presents a framework for analyzing uniform program properties (relating to the content of data structures rather than to the structures themselves) in a high-order functional language with recursive data structures. The development starts from a set of general (logic and type-specific) rules and from rules that pertain to the particular analysis being undertaken. Strictness is the central property under consideration throughout, but other properties considered include binding time and dataflow analyses.

Notation is a potential problem in any work that bridges so many topics. The “box” and “diamond” symbols have nonstandard interpretations as do t (here indicating that we know everything--no specific information) and f (here indicating “undefined”). These are reasonable, but initially confusing, particularly because t and f are distinct from the Boolean constants. The author does point this out.

For each expression in the language, we can derive a normal form consisting of a disjunction of irreducible formulas. Entailment gives rise to provable equality, which is then used to quotient out equivalent expressions, giving a partial-order semantics. Hence, we can calculate an abstract interpretation for each expression in terms of lower sets. Although there are issues that make direct application of the theory impractical, the results are interesting and can be used in conjunction with the work of others. The paper is well motivated and includes adequate explanations. The relationship between this research and the work of others is discussed at length. Its association with tensor products is particularly relevant.