Strictness Logic and Polymorphic Invariance

8 years 10 months ago
Strictness Logic and Polymorphic Invariance
We describe a logic for reasoning about higher-order strictness properties of typed lambda terms. The logic arises from axiomatising the inclusion order on certain closed subsets of domains. The axiomatisation of the lattice of strictness properties is shown to be sound and complete, and we then give a program logic for assigning properties to terms. This places work on strictness analysis via type inference on a firm theoretical foundation. We then use proof theoretic techniques to show how the derivable strictness properties of different instances of polymorphically typed terms are related.
P. N. Benton
Added 10 Aug 2010
Updated 10 Aug 2010
Type Conference
Year 1992
Where LFCS
Authors P. N. Benton
Comments (0)