Going to try and formalize in HOLCF the construction http://arxiv.org/abs/1403.0749 and see what breaks/doesn't break when there's non-termination