Comment by siraben

This discussion reminds me of the style guide for a Coq PL formalization project:

> No unicode or infix operators for judgement forms. When I use them in my proofs they make perfect sense, but when you use them in yours they're completely unreadable.

Computers (parsers, rather) are extremely sensitive to notation, and indeed in this project they eschew greek letters and unicode altogether, however it makes things more verbose, but it is almost certain that the authors communicate the ideas in paper with notation like Γ ⊢ e : σ instead of `TYPE Gamma e s`.