Yes, I'm aware of those papers. I've read many including the one that you linked. As far as I'm aware, while you can use the strict definition (is there, in the

Yes, I'm aware of those papers. I've read many including the one that you linked. As far as I'm aware, while you can use the strict definition (is there, in the metalanguage, the creation of an AST?) they're often discussed as more of a continuum. HOAS is a great example. There is the creation of an AST, but perhaps the most important and tricky part of any AST, the binding system, is left to the metalanguage. For that reason exactly I'm happy to say that HOAS is "shallower" than, say, a de Bruijn indexed binding system.