[jonsterling]

That paper is just a bit of bureaucracy which demonstrates that total programs behave the same in a total language as when they are embedded into a partial language (which is an intuitive result, and it's nice that they worked out the details!). It's also a nice demonstration of the logical relations proof technique.

But sadly this paper is pulled out all the time by people who I suspect don't understand what is going on, to justify sleight of hand & dodgy reasoning which has little to do with the result in the paper. (Not claiming that's what's happening in the above comment! But I bristle a bit when I see this paper come up in amateur/Haskell circles.)