Do you want to define syntax with binders in Agda but have no idea whether to use de Bruijn indices, nominal sets, HOAS, or yet something else?
Well then, good news! I have a new blog post for you: jesper.sikanda.be/posts/1001-syn
4
40
133
Conversation
Super great overview, thanks for this! I'm still pretty happy with defunctionalized NbE (with indices in terms and levels in values). Makes implementation much easier, and is good for performance, but I dunno how it fares for formalization work.
3
6
What does it mean to be defunctionalised NBE? Does that refer to your encoding of closures?
1
Referring to how it is described in “Implementing a Modal Dependent Type Theory”, section 3.1: jonmsterling.com/pdfs/modal-mlt – but I might be misusing the term. I think I'm more just referring to the approach described in Abel's habilitation thesis: cse.chalmers.se/~abela/habil.p