An operational semantics of lazy evaluation for analysis

Lazy evaluation has become a common method of evaluation for implementing functional languages. However, there has been no model of lazy evaluation established that is more abstract than an abstract machine. The purpose of this work is to develop an operational semantics capturing lazy evaluation which is suitable for reasoning. The semantics is described as a natural semantics. The equivalence of the semantics with a call-by-name natural semantics is given to demonstrate its computational correctness. Certain properties of the semantics, such as a characterization of normal forms and a subject reduction theorem, are also given. In order to demonstrate the usefulness of the semantics and its suitability for reasoning, the semantics is used to develop a static analysis.;A common approach to static analysis is the development of an abstract interpretation over a non-standard denotational semantics. Though the information yielded by this analysis is correct with respect to the non-standard denotational semantics automatically, there is no guarantee that the non-standard semantics itself is correct. In this work, an analysis is developed that is based on an operational definition of the desired information which is defined in terms of the evaluations generated by the operational semantics. An instrumented version of the semantics is also developed to capture the desired information. The instrumented semantics is proved to be correct with respect to the operational definition. Then a type system is developed which captures the information as types of expressions. The correctness of the type system with respect to the instrumented semantics is also shown. Thus an analysis is developed which is proven correct with respect to an operational definition of the desired information.