I remember that I read a related paper a couple of months before, that paper discuss "stationary" field, which is similar to to this.
similar mechnism include the java standard "final" field, which is some what too restricted.
So in summary, there are three class of such mechnism:
final,too strong
stationary
quie scing
Such mechnism can prevent those variables from been initialied or writen more than one time.typical application include OO system that need to initite newlly allocated object.
Its slide describe an interesting relation between type system and effect system, the formmer one describe "what is the object",while the later one describe "how the object behave"