Fact Fact:

fact: "r.{eax:int, esp:(t::r)}

where t ={eax:int, esp:r}

Because r is abstract, if you call fact, then either:

(a) it never returns

(b) it returns the stack in the same state it was

in before the call.

Result follows from Reynold’s Parametricity theorem.

Previous slide

Next slide

Back to first slide

View graphic version