Judgement
Backlinks
Weakening Rule
Sequent Calculus
Bidirectional Type Theory