We establish an equivalence between two techniques for analysing higher-order functional programs: abstract interpretation and non-standard type inference. The equivalence is based on an axiomatic presentation of the lattices used in abstract interpretation. This axiomatization forms the basis of a program logic for deducing properties of expressions in a simply typed lambda calculus enriched with fixed points and constants. The main result of the paper is that the strictness logic is sound and complete with respect to the abstract interpretation thus proving that strictness analysis by type inference and by abstract interpretation are equally powerful techniques. We then show how a similar result can be obtained for binding-time analysis.
展开▼
