# Tag Info

Lennart Augustsson and Kent Petersson 1994 present syntax and type rules for a small functional language which is basically just lambda calculus with GADTs. They have two kinds of judgments, one to indicate that "the expression e has type T in the type environment $\Gamma$" and the other to indicate that "the declaration d generates the type environment \$\...