Introduction Rule
Backlinks
Right Rule
Sequent Calculus
Bidirectional Type Theory