<p>Amal Ahmed's very readable <a href="http://www.cs.princeton.edu/research/techreps/TR-713-04">thesis dissertation</a> could be a nice start.</p>

CC BY-SA 3.0
2013-04-14T10:00:13.750Z
Amal Ahmed also gave lectures on step-indexed logical relations at the Oregon Programming Languages Summer School. The videos are online: http://www.cs.uoregon.edu/research/summerschool/summer12/curriculum.html
namin
CC BY-SA 3.0
2013-03-21T14:17:01.457Z
2013-03-21T14:17:01.457Z
cody
<p>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 <a href="http://delivery.acm.org/10.1145/1200000/1190235/p109-appel.pdf?ip=137.132.3.10&amp;acc=AUTHOR-IZED&amp;CFID=194763560&amp;CFTOKEN=29858435&amp;__acm__=1363863619_b7110046a48ec37b7fe67cba12d248ef" rel="nofollow">Very Modal Model</a> 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.</p>

<p>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.</p>

<reference-request><pl.programming-languages><program-verification><formal-methods><operational-semantics>
Step-indexing: Where to begin?
C.E.Sally
# Step-indexing: Where to begin?

(Asked by: username_0 on 2013-03-21)

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](http://delivery.acm.org/10.1145/1200000/1190235/p109-appel.pdf?ip=137.132.3.10&acc=AUTHOR-IZED&CFID=194763560&CFTOKEN=29858435&__acm__=1363863619_b7110046a48ec37b7fe67cba12d248ef) 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.

**Tags:** reference-request, pl.programming-languages, program-verification, formal-methods, operational-semantics

---

## 1 answers

### Answer by username_1 on 2013-03-21. Score: 10 | Accepted answer

Amal Ahmed's very readable [thesis dissertation](http://www.cs.princeton.edu/research/techreps/TR-713-04) could be a nice start.

> **Comments:**
> **username_2**: Amal Ahmed also gave lectures on step-indexed logical relations at the Oregon Programming Languages Summer School. The videos are online: http://www.cs.uoregon.edu/research/summerschool/summer12/curriculum.html  

---

