## User login## Navigation |
## A Type-theoretic Foundation for Programming with Higher-order Abstract Syntax and First-class Substitutions
A Type-theoretic Foundation for Programming with Higher-order Abstract Syntax and First-class Substitutions by Brigitte Pientka, appeared in POPL 08.
Higher-order abstract syntax (HOAS) is a simple, powerful technique for implementing object languages, since it directly supports common and tricky routines dealing with variables, such as capture-avoiding substitution and renaming. This is achieved by representing binders in the object-language via binders in the meta-language. However, enriching functional programming languages with direct support for HOAS has been a major challenge, because recursion over HOAS encodings requires one to traverse - abstractions and necessitates programming with open objects.Its been a while since I posted, but this paper appears that it may be of interest to some members of this community. It looks interesting to me, but I just wish I understood all the terminology. I don't know what "open objects" are, and why they are a problem. I don't understand what HOAS is. I don't even know what binders are. The list goes on. I surely can't be the only person who is interested, but feels that this is just out of their grasp. I bet that I probably could understand these things with a minimum of explanation, given I have experience implementing languages. If anyone is interested in rephrasing the abstract in more basic terms, I would be very appreciative. [Edit: corrected spelling of Brigitte Pientka. My apologies.] |
## Browse archives## Active forum topics |

## Recent comments

2 hours 23 min ago

5 hours 59 min ago

6 hours 5 min ago

6 hours 8 min ago

6 hours 52 min ago

7 hours 26 min ago

7 hours 56 min ago

8 hours 15 min ago

12 hours 34 min ago

13 hours 20 min ago