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

[Jason -Zhong Sheng- Hu]

many formalization boils down to de Bruijn indices I think.

locally nameless representation is quite different but it could be very counter intuitive. for example, we might consider a derivation is a tree the height of which can be measured by natural number but locally nameless representation might break this assumption.

Thanks,
Jason Hu
https://hustmphrrr.github.io/
________________________________
From: Agda <agda-bounces at lists.chalmers.se> on behalf of Andreas Abel <andreas.abel at ifi.lmu.de>
Sent: April 24, 2020 10:04 AM
To: Joey Eremondi <joey.eremondi at gmail.com>; Agda mailing list <agda at lists.chalmers.se>
Subject: Re: [Agda] What do you use for variable binding in 2020?

De Bruijn indices.

 > * Type/scope safe universes: I haven't fully grokked this one, but it's
 > got a lot of smart people behind it.

This paper is a systematization of de Bruijn indices.  (If I understand
it correctly.)

On 2020-04-22 06:07, Joey Eremondi wrote:
> 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!
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200424/d42977dc/attachment.html>