8
$\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$

1 Answer 1

10
$\begingroup$

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

$\endgroup$
1

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.