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
7 hours 7 min ago
8 hours 35 min ago
15 hours 5 min ago
17 hours 49 min ago
1 day 1 hour ago
1 day 2 hours ago
1 day 4 hours ago
1 day 6 hours ago
1 day 7 hours ago
1 day 7 hours ago