1
Jesper Cockx - 1001 Representations of Syntax with Binding
source link: https://jesper.sikanda.be/posts/1001-syntax-representations.html
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
Overview and conclusion
The goal of this blog post was mainly to give an overview of the various different approaches one could use when defining syntax with binders in Agda. Below is a table summarizing with the approaches I described, plus the benefits they provide to the programmer:
First-order representation: does the representation avoid the use of meta-level functions as part of the data structure? If not, it can be difficult or impossible to do things like checking equality of terms or pretty-printing.
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK