  Step-indexed semantic models of types were proposed as an alternative to
purely syntactic safety proofs using subject-reduction. Building upon the work
by Appel and others, we introduce a generalized step-indexed model for the
call-by-name lambda calculus. We also show how to prove type safety of general
recursion in our call-by-name model.
