 The paper Areces, Blackburn, Huertas, and Manzano (2014) deals with a hybrid-logical version of higher-order modal logic (that is, modal logic built over Church’s simple theory of types). Axiom systems are given and completeness is proved wrt. Henkin-type semantics. The paper Blackburn, Huertas, Manzano, and Jørgensen (2014) extends these results to encompass the downarrow binder and gives translations to and from the bounded fragment of first-order logic (see above).