A theory of lazy λ-calculus is developed as a basis for lazy functional programming languages. This is motivated by a mismatch between the "standard" (i.e., sensible) theory of the classical λ-calculus and the practice of lazy functional programming. Part I sets up the fundamentals of the lazy λ-calculus starting from the pure lazy language λl. We develop the rudiments of weakly sensible λ-theory and characterize λl as the maximal such theory. The axiomatic framework of our theory is based on the notion of applicative transition systems which gives rise to lazy λ-models. The subclass of lazy λ-models which are operationally extensional are called lambda transition systems (lts′s). The canonical model of the lazy λ-calculus is the initial solution to the domain equation D ≅ [D → D]⊥. We set up the domain logic corresponding to the same type expression. In part II, we recast the full abstraction problem in the lazy λ-calculus. The pure lazy language λl is not equationally fully abstract w.r.t. D. In fact, λl, λlω, (a labelled version of λl), and λlc (λl augmented with a convergence testing constant) are all not equationally fully abstract w.r.t. D. We illustrate two approaches to full abstraction: