User loginNavigation 
A Typetheoretic Foundation for Programming with Higherorder Abstract Syntax and Firstclass Substitutions
A Typetheoretic Foundation for Programming with Higherorder Abstract Syntax and Firstclass Substitutions by Brigitte Pientka, appeared in POPL 08.
Higherorder 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 captureavoiding substitution and renaming. This is achieved by representing binders in the objectlanguage via binders in the metalanguage. 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 archivesActive forum topics
New forum topics

Recent comments
8 hours 3 min ago
15 hours 11 min ago
1 day 10 hours ago
2 days 17 hours ago
3 days 3 hours ago
3 days 13 hours ago
3 days 16 hours ago
3 days 17 hours ago
3 days 20 hours ago
4 days 48 min ago