Fully abstract models of the lazy lambda calculus

Much of what is known about the model theory and proof theory of the λ-calculus is sensible in nature, i.e. only head normal forms are semantically meaningful. However, most functional languages are lazy, i.e. programs are evaluated in normal order to weak head normal forms. The author develops a theory of lazy or strongly sensible λ-calculus that corresponds to practice. A general method for constructing fully abstract models for a class of lazy languages is illustrated. A formal system called λβC (λβ-calculus with convergence testing C) is introduced, and its properties are investigated