Another very interesting opportunity given by functional languages, especially typed-functional languages is higher order abstract syntax. We all know that the theory of syntax is a very well established theory, especially when we consider formal grammars. But formal grammars deal only with context-free features of languages. While we all know that programming languages especially modern programming languages, high-level programming languages have grammars which need to take into account many context dependent features. So it is an open problem of how to specify programming languages so as to take into account also the context dependent features. And here again typed-functional languages do offer a possible solution and this is called "higher order abstract syntax". This technique allows in fact to capture across different formal systems all the details of variable management and these are alpha conversion, capture-avoiding substitution, instantiation, binding operations and so on. Using "higher order abstract syntax" we can delegate all these features to the metalanguage and thus having implemented and editor or a proof-assistant for the metalanguage once and for all we have solved all future problems having to do with the specification of the syntax for specific languages.

---