## 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

10 hours 58 min ago

14 hours 45 min ago

14 hours 51 min ago

22 weeks 1 day ago

26 weeks 3 days ago

28 weeks 22 hours ago

28 weeks 22 hours ago

30 weeks 5 days ago

35 weeks 3 days ago

35 weeks 3 days ago