I took it as completely serious. Variation in notation for this kind of thing is a severe obstacle to understanding a paper. It also means the authors are missi

I took it as completely serious. Variation in notation for this kind of thing is a severe obstacle to understanding a paper. It also means the authors are missing out on useful tooling for checking the correctness of their notation, let alone their models. Redex takes this in an interesting direction, allowing you to write your language models in S-expressions, run them, test them, and get LaTeX out automatically. See https://redex.racket-lang.org/ https://redex.racket-lang.org/ and https://eecs.northwestern.edu/~robby/lightweight-metatheory/popl2012-kcdeffmrtf.pdf https://eecs.northwestern.edu/~robby/lightweight-metatheory/... .