2412 a non-trivial language that uses Chargu\'eraud's idea. |
2412 a non-trivial language that uses Chargu\'eraud's idea. |
2413 |
2413 |
2414 Another technique for representing binding is higher-order abstract syntax |
2414 Another technique for representing binding is higher-order abstract syntax |
2415 (HOAS), which for example is implemented in the Twelf system \cite{pfenningsystem}. |
2415 (HOAS), which for example is implemented in the Twelf system \cite{pfenningsystem}. |
2416 This representation technique supports very elegantly many aspects of |
2416 This representation technique supports very elegantly many aspects of |
2417 \emph{single} binding, and impressive work by Lee et al ~\cite{LeeCraryHarper07} |
2417 \emph{single} binding, and impressive work by Lee et al~\cite{LeeCraryHarper07} |
2418 has been done that uses HOAS for mechanising the metatheory of SML. We |
2418 has been done that uses HOAS for mechanising the metatheory of SML. We |
2419 are, however, not aware how multiple binders of SML are represented in this |
2419 are, however, not aware how multiple binders of SML are represented in this |
2420 work. Judging from the submitted Twelf-solution for the POPLmark challenge, |
2420 work. Judging from the submitted Twelf-solution for the POPLmark challenge, |
2421 HOAS cannot easily deal with binding constructs where the number of bound |
2421 HOAS cannot easily deal with binding constructs where the number of bound |
2422 variables is not fixed. For example, in the second part of this challenge, |
2422 variables is not fixed. For example, in the second part of this challenge, |