I have tagged some question about type-theory with area tag pl.programming-lang but almost always they get removed (right now there is only one question with both tags), so it seems that there is a disagreement here. The other option is to use lo.logic. Isn't type-theory considered a PL topic? I would think that most of type-theory works, especially more practicable ones, are published using PL subject classification not logic, so I am confused.
Which area tag should we use for type-theory questions (and when)?