[Agda] What do you use for variable binding in 2020?

[Joey Eremondi]

I'm modelling a programming language/core-calculus in Agda, and I'm
wondering what people use to model binding and name capture?
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.

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.

I'm aware of:

* De Bruijn/ Locally Nameless: seems pretty solid, but requires
implementing substitution and other traversals myself, possibly twice.
* 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
* Shifted Names: looks promising, but I'm not sure how mature this idea is
http://tydeworkshop.org/2019-abstracts/paper16.pdf
* Type/scope safe universes: I haven't fully grokked this one, but it's got
a lot of smart people behind it. https://dl.acm.org/doi/10.1145/3236785

What do you use? What do you like? What has tutorials / code examples /
libraries?

Thanks!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200421/5402e438/attachment.html>