7
$\begingroup$

I have tagged some question about with area tag 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 . 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)?

$\endgroup$
0

2 Answers 2

Reset to default
6
$\begingroup$

There seems to be more than one question with both the and tags.

In any case, type theory is a branch of logic that has seen many applications in programming languages, namely, as type systems. Type theory questions that are not programming language questions often take the form of questions about automated reasoning or proof assistants and their underlying theory. Even though there is a programming language for specifying the input to such proof assistants, PL and type theory people wouldn't consider these to be PL questions.

Also, the fact that a question mentions types, does not necessarily mean it is about type theory, especially if it is a programming languages question. Types are a part of programming languages, but this doesn't mean that every programming languages question about types is a type theory question.

I'll scan through the questions we have thus far and see whether I can draw any additional conclusions.

$\endgroup$
4
  • 1
    $\begingroup$ so then depending on the context, we could use either tag ? $\endgroup$
    – Suresh Venkat
    May 24, 2011 at 20:56
  • 2
    $\begingroup$ Indeed. Or both. $\endgroup$
    – Dave Clarke
    May 25, 2011 at 6:28
  • $\begingroup$ Thanks Dave for the clarification. $\endgroup$
    – Kaveh
    May 26, 2011 at 2:48
  • $\begingroup$ @SureshVenkat , Dave, Kaveh, in case if any of you hadn't seen this yet: Stack Exchange will very soon be launching a brand new site dedicated to computer-assisted proofs: please use my referral link here if you're considering to get an invitation to the Private Beta! I also posted on Meta about this. $\endgroup$
    – user1271772
    Jan 16, 2022 at 4:46
1
$\begingroup$

I don't understand why isn't ok ? can any of the PL folks clarify ?

$\endgroup$
1
  • 4
    $\begingroup$ You can think of it this way: type theory is a part of logic and applied type theory is a part of programming languages. $\endgroup$
    – Dave Clarke
    May 24, 2011 at 7:43

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .