<div dir="ltr"><div>I'm modelling a programming language/core-calculus in Agda, and I'm wondering what people use to model binding and name capture?</div><div> I'm familiar with a few techniques in general, but I'm wondering if specific ones works better in Agda, or have libraries to support them, or at least good examples of code using them.</div><div><br></div><div>My language has a lot of constructs, so the ideal for me is something that either doesn't require me to implement substitution myself, or where I can do it generically, so I'm not writing a ton of boiler plate.<br></div><div><br></div><div>I'm aware of:<br></div><div><br></div><div>* De Bruijn/ Locally Nameless: seems pretty solid, but requires implementing substitution and other traversals myself, possibly twice.</div><div>* PHOAS: handles capturing and shadowing easily, but seems to be more popular with Coq? Not sure how it scales modelling to things like type rules and small-step semantics<br></div><div>* Shifted Names: looks promising, but I'm not sure how mature this idea is <a href="http://tydeworkshop.org/2019-abstracts/paper16.pdf">http://tydeworkshop.org/2019-abstracts/paper16.pdf</a></div><div>* Type/scope safe universes: I haven't fully grokked this one, but it's got a lot of smart people behind it. <a href="https://dl.acm.org/doi/10.1145/3236785">https://dl.acm.org/doi/10.1145/3236785</a></div><div><br></div><div>What do you use? What do you like? What has tutorials / code examples / libraries?</div><div><br></div><div>Thanks!<br></div></div>