We’ve sent off the final version of Contracts Made Manifest. There have been quite a few improvements since submission, the most important of which is captured by Figure 1 from our paper:
Our submission only addressed lax λC, where we had an inexact translation φ into λH and an exact translation ψ out of λH. We show a dual situation for picky λC, where φ is exact and ψ is inexact. Intuitively, languages farther to the right on the “axis of blame” are pickier. Translating from right to left preserves behavior exactly, but left-to-right translations generate terms that can blame more than their pre-images. (There are examples in the paper.) I should note that lax and picky λC seem to be the extremes of the axis of blame: I don’t see a natural way to be laxer than lax λC or pickier than picky λC.
We also show that restricting these calculi to first-order dependency leaves them exactly equivalent; before, we could only show an exact equivalence by eliminating all dependency.