There was this Manifest Security meeting happening today that I sat in on. Neat stuff. I think I finally understand exactly how Henry and Frank's paper can be 'deconstructed', and it's quite simple. Make a poset with judgments knows_K, has_K, asserts_K, valid, true, lax. What the paper calls "hyp" on the left is the same as what it calls "true" on the right, and I'm calling them both just "true". Valid and knows_K are unrestricted, and the rest are linear. Axiomatize the stronger-than relation by taking for every K all of
knows_K ≥ has_K
knows_K ≥ valid
valid ≥ true
has_K ≥ true
true ≥ asserts_K
true ≥ lax
and taking the reflexive, transitive closure. Then all the connectives are defined "at true". The connectives [[ ]], [ ], < >, !, and { } are defined as round trips through knows, has, asserts, valid, and lax, departing from and returning to true.

Afterwards tagged along with rwh and ben pierce and one of pierce's students for dinner, much technical conversation ensued.