This problem session will present a mechanical formalization of step-indexed logical relations using a small-step environment-based semantics.