Local soundness and completeness are PL-like properties

Currently, I'm trying to write up a tech report that clearly and fully present a peculiar modal logic that I discovered with the help of another graduate student last spring. In this tech report, I'm trying to closely follow what I think is correct to call the judgmental methodology , a philosophy for designing logics that was first outlined by Martin Lof in the 1983 Siena lectures and was refined by Pfenning and Davies in the 1999 paper "A Judgmental Reconstruction of Modal Logic."

Something that I think I knew but that I hadn't ever fully internalized is the degree to which the developments and checks recommended by the judgmental methodology are much closer to what you want when defining a programming language (where type safety - progress and preservation - are primary concerns) than what you want when defining a logic (where consistency, which is a sort of normalization property, is a big concern).

A really, really high level picture of the methodology followed by Pfenning and Davies is this:

• Define a substitution principle
• Show that everything that looks it should be a reducible expression (redex) is actually, you know, reducible (local soundness)
• Show that everything that has an interesting type can be η-expanded (local completeness)
• Check that the substitution principle which you claimed to be true and possibly used in the previous two steps actually holds

Now, as it turns out, proving the property of local completeness gets you most of the way there to the property called global completeness, but local soundness is woefully inadequate to get what you might call global soundness, the property that given a proof with redexes you can reduce redexes over and over until you get a proof with no redexes anymore. What I think local soundness ensures is that you'll always be able to keep reducing things that looks like redexes unless there aren't any more things that look like redexes. But this is just a progress property, that everything that "looks like a redex" actually is one. The combined local soundness proofs additionally can be seen as the cases of a variant form of the preservation theorem called subject reduction - this means that the local soundness proofs demonstrate both (a sort of) progress property and (a sort of) preservation property.

Is it really the case that the only "more interesting" part of type safety theorems is the fact that programming languages have values - places where, in practice, you want to stop with all of this reducing business - and the safety proof has to show that these uses of values are somehow consistent with the desired progress theorem? And has the "progress-ey" part of local soundness been considered elsewhere? Certainly the preservation-ey part is well-known enough to have its own name, "subject reduction." It seems like the kind of discussion that would be natural to find in the hybrid child of Proofs and Types and TAPL, but I don't believe such a book exists.