6
$\begingroup$

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.

$\endgroup$
7
$\begingroup$

Amal Ahmed's very readable thesis dissertation could be a nice start.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.