Coauthor of the "Modelling ..." paper here. Happy to answer questions!

How is hygiene handled? For example, does this relate to or incorporate some of the "Bindings as Sets of Scopes" work?

Hygiene is deliberately omitted.

Why? Because there are various different ways of handling hygiene, including not providing hygiene at all. A foundational model of MP should not 'hard-code' any specific approach towards hygiene.

Our model can be used as a basis to implement any approach to hygiene that is of interest.

Oh, and given that Christian Urban is a coauthor, are you using nominal techniques?

We have an implementation in Nominal Isabelle/HOL, but it's not used in the paper.