4 ms·

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

• auggierose 9y ago
  How is hygiene handled? For example, does this relate to or incorporate some of the "Bindings as Sets of Scopes" work?
  • xgk 9y ago
    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.
    • xgk 9y ago
      Our model can be used as a basis to implement any approach to hygiene that is of interest.
• auggierose 9y ago
  Oh, and given that Christian Urban is a coauthor, are you using nominal techniques?
  • xgk 9y ago
    We have an implementation in Nominal Isabelle/HOL, but it's not used in the paper.