Bidirectional Type Theory

A bidirectional type theory is a type theory where the Judgement $\Gamma\vdash e:A$ comes in two forms: a "check" form $\Gamma\vdash e:A\Uparrow$ and a "synthesis" form $\Gamma\vdash e:A\Downarrow$. This allows the theory to enforce certain syntactic constraints on terms; EG: that they have no $\beta$-redexes.

Typically, the check rules are the Introduction Rules and the synthesis rules are the Elimination Rules, though some care must be taken with the Structural Rules. For instance, there are 4 possible forms of the rule for Let Bindings!