Mixed lazy/strict graph semantics

Abstract. Explicitly enforcing strictness is often used by functional pro-grammers as an important tool for making applications fit time and space efficiency requirements. Few functional programmers however, are famil-iar with the consequences of explicitly enforcing strictness for formal reasoning about their programs. Some “folklore ” knowledge has emerged but this is based on experience rather than on rigid proof. Up to now no formal model has been available for reasoning about enforcing strict-ness in denotational and operational semantics. This greatly hampered formal reasoning on mixed lazy/strict programs. This paper presents a model for formal reasoning with enforced strictness based on John Launchbury’s lazy graph semantics. Lazy graph seman-tics are widely considered to be essential for lazy functional program-ming languages. In this paper Launchbury’s semantics are extended with an explicit strict let construct. Correctness and adequacy of our mixed lazy/strict graph semantics is proven. Using these mixed semantics we formalise and prove some of the available “folklore ” knowledge. 1 Introduction an