<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body dir="ltr">
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
many formalization boils down to de Bruijn indices I think.</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
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.<br>
</div>
<div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div id="Signature">
<div></div>
<div id="divtagdefaultwrapper" dir="ltr" style="font-size: 12pt; color: rgb(0, 0, 0); font-family: Calibri, Arial, Helvetica, sans-serif;">
<font size="3"><b>Thanks,</b></font></div>
<div dir="ltr" style="font-size: 12pt; color: rgb(0, 0, 0); font-family: Calibri, Arial, Helvetica, sans-serif;">
<font size="3"><b>Jason Hu</b></font></div>
<div dir="ltr" style="font-size: 12pt; color: rgb(0, 0, 0); font-family: Calibri, Arial, Helvetica, sans-serif;">
<font size="3"><b><a href="https://hustmphrrr.github.io/" style="">https://hustmphrrr.github.io/</a></b></font><br>
<font size="3"><b></b></font><font style="font-size:12pt" size="3"><span style="color: rgb(69, 129, 142);"><span style="font-family:trebuchet ms,sans-serif"><b><a target="_blank" style=""></a></b></span></span></font></div>
</div>
</div>
<div id="appendonsend"></div>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Agda <agda-bounces@lists.chalmers.se> on behalf of Andreas Abel <andreas.abel@ifi.lmu.de><br>
<b>Sent:</b> April 24, 2020 10:04 AM<br>
<b>To:</b> Joey Eremondi <joey.eremondi@gmail.com>; Agda mailing list <agda@lists.chalmers.se><br>
<b>Subject:</b> Re: [Agda] What do you use for variable binding in 2020?</font>
<div> </div>
</div>
<div class="BodyFragment"><font size="2"><span style="font-size:11pt;">
<div class="PlainText">De Bruijn indices.<br>
<br>
> * Type/scope safe universes: I haven't fully grokked this one, but it's<br>
> got a lot of smart people behind it.<br>
<br>
This paper is a systematization of de Bruijn indices. (If I understand <br>
it correctly.)<br>
<br>
On 2020-04-22 06:07, Joey Eremondi wrote:<br>
> I'm modelling a programming language/core-calculus in Agda, and I'm <br>
> wondering what people use to model binding and name capture?<br>
> I'm familiar with a few techniques in general, but I'm wondering if <br>
> specific ones works better in Agda, or have libraries to support them, <br>
> or at least good examples of code using them.<br>
> <br>
> My language has a lot of constructs, so the ideal for me is something <br>
> that either doesn't require me to implement substitution myself, or <br>
> where I can do it generically, so I'm not writing a ton of boiler plate.<br>
> <br>
> I'm aware of:<br>
> <br>
> * De Bruijn/ Locally Nameless: seems pretty solid, but requires <br>
> implementing substitution and other traversals myself, possibly twice.<br>
> * PHOAS: handles capturing and shadowing easily, but seems to be more <br>
> popular with Coq? Not sure how it scales modelling to things like type <br>
> rules and small-step semantics<br>
> * Shifted Names: looks promising, but I'm not sure how mature this idea <br>
> is <a href="http://tydeworkshop.org/2019-abstracts/paper16.pdf">http://tydeworkshop.org/2019-abstracts/paper16.pdf</a><br>
> * Type/scope safe universes: I haven't fully grokked this one, but it's <br>
> 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><br>
> <br>
> What do you use? What do you like? What has tutorials / code examples / <br>
> libraries?<br>
> <br>
> Thanks!<br>
> <br>
> _______________________________________________<br>
> Agda mailing list<br>
> Agda@lists.chalmers.se<br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
> <br>
_______________________________________________<br>
Agda mailing list<br>
Agda@lists.chalmers.se<br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div>
</span></font></div>
</body>
</html>