jumps
add continuations
S : stmt ? formula ? formula
translation becomes
S ? a ; b ? ? = S ? a ? (S ? b ? ?)
S ? if p a b ? ? = (P ? p ? ? S ? a ? ?) ? (!P ? p ? ? S ? b ? ?)
S i ? while p { a } ? ? = (P ? p ? ? S ? a ? ; S i-1 ? while p { a } ? ? ) ? ! P ? p ? ? ?
S 0 ? while p { a } ? ? = ! P ? p ? ? ?
S ? v = t ? ? = Close (v’ = E ? t ?) ; ?
S ? return t ? ? = Close (result = E ? t ?)
cleaner treatment of null derefs
instead of null, make fields partial
S ? t.f = u ? ? = (some E ? t ? ? E ? t ? . f’ = E ? u ? ; ?) ? no E ? t ?