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.