<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
Hi Joey,
<div class=""><br class="">
</div>
<div class="">These days I’m using de Bruijn but in the style of PLFA and I’m relatively happy with it.</div>
<div class="">However, if you need any non-trivial lemmas about substitution (such as commutativity</div>
<div class="">of substitution), then it might be worth your while to use my library to define your</div>
<div class="">abstract syntax trees and substitution functions:</div>
<div class=""><br class="">
</div>
<div class=""><a href="https://github.com/jsiek/abstract-binding-trees" class="">https://github.com/jsiek/abstract-binding-trees</a></div>
<div class=""><br class="">
</div>
<div class="">(I note that there are more sophisticated libraries for this kind of thing, but</div>
<div class="">I’ve found it difficult to understand the other ones.)</div>
<div class=""><br class="">
<div>Cheers,</div>
<div>Jeremy</div>
<div><br class="">
<blockquote type="cite" class="">
<div class="">On Apr 22, 2020, at 12:07 AM, Joey Eremondi <<a href="mailto:joey.eremondi@gmail.com" class="">joey.eremondi@gmail.com</a>> wrote:</div>
<br class="Apple-interchange-newline">
<div class="">
<div dir="ltr" class="">
<div class="">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 class="">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 class=""><br class="">
</div>
<div class="">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 class="">
</div>
<div class=""><br class="">
</div>
<div class="">I'm aware of:<br class="">
</div>
<div class=""><br class="">
</div>
<div class="">* De Bruijn/ Locally Nameless: seems pretty solid, but requires implementing substitution and other traversals myself, possibly twice.</div>
<div class="">* 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 class="">
</div>
<div class="">* Shifted Names: looks promising, but I'm not sure how mature this idea is
<a href="http://tydeworkshop.org/2019-abstracts/paper16.pdf" class="">http://tydeworkshop.org/2019-abstracts/paper16.pdf</a></div>
<div class="">* 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" class="">https://dl.acm.org/doi/10.1145/3236785</a></div>
<div class=""><br class="">
</div>
<div class="">What do you use? What do you like? What has tutorials / code examples / libraries?</div>
<div class=""><br class="">
</div>
<div class="">Thanks!<br class="">
</div>
</div>
_______________________________________________<br class="">
Agda mailing list<br class="">
<a href="mailto:Agda@lists.chalmers.se" class="">Agda@lists.chalmers.se</a><br class="">
https://lists.chalmers.se/mailman/listinfo/agda<br class="">
</div>
</blockquote>
</div>
<br class="">
<div class="">
<div dir="auto" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
<div style="color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
<div style="color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
<div style="color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
<div class=""><span style="font-family: Menlo; font-size: medium; orphans: 2; widows: 2;" class="">__________________________________________</span><br style="font-family: Menlo; orphans: 2; widows: 2;" class="">
<span style="font-family: Menlo; orphans: 2; widows: 2;" class="">Jeremy G. Siek <<a href="mailto:jsiek@indiana.edu" class="">jsiek@indiana.edu</a>></span><br style="font-family: Menlo; orphans: 2; widows: 2;" class="">
<span style="font-family: Menlo; orphans: 2; widows: 2;" class="">Professor</span><br style="font-family: Menlo; orphans: 2; widows: 2;" class="">
<span style="font-family: Menlo; orphans: 2; widows: 2;" class="">Luddy School of Informatics, Computing, and Engineering</span><br style="font-family: Menlo; orphans: 2; widows: 2;" class="">
<span style="font-family: Menlo; orphans: 2; widows: 2;" class="">Indiana University Bloomington</span><br style="font-family: Menlo; orphans: 2; widows: 2;" class="">
<span style="font-family: Menlo; orphans: 2; widows: 2;" class=""><a href="http://homes.soic.indiana.edu/jsiek/" class="">http://homes.soic.indiana.edu/jsiek/</a></span><br class="">
</div>
<div class=""><span style="font-family: Menlo; orphans: 2; widows: 2;" class=""><br class="">
</span></div>
</div>
</div>
<br class="Apple-interchange-newline">
</div>
<br class="Apple-interchange-newline">
</div>
<br class="Apple-interchange-newline">
<br class="Apple-interchange-newline">
</div>
<br class="">
</div>
</body>
</html>