I am about to begin a verification project (for MIPS) with my professor (I am a senior undergraduate) and have been told that the soundness proof for the program logic we need will probably involve step-indexing. I have read the Very Modal Model paper by Appel et al. and after a short tutorial by my prof, I think I have a basic understanding of step-indexing. However it has been kind of slow going. Especially when the $\mu$ operator and contravariance come up.
I would like to ask for either the original papers where step-indexing was introduced (from what I understand it traces back to the 50-60s? but am having trouble finding them) or if someone can point out a tutorial, that would also be great.
