I’ve waffled on higher education for PL because of my [incorrect?] perception that academia is fixated on type theory as a way to solve everything. I generally like it but I don’t know if I like it enough to do a PhD in it. Is this true?
By fixated, do you mean “academia has an obsession with type theory, and tries to use it where it is inappropriate”? I don’t get that vibe, but then again, its my primary field so I may be biased :)
If you want to study PL theory you should expect to encounter type theory and the lambda calculus. Otherwise, it’s up to you. Unless you work in a big group you’re going to have some freedom in selecting the problem you want to solve and how you want to solve it, although it’ll need to be related to whatever your adviser has a grant for. Look at the faculty of schools you’re interested in and see what they’re publishing on.
Depends on the school and its goals. Many are about whats practical or just looks like it for grant money. You see a lot of Java, C#, etc there. Quite a few on Scheme with DSL’s. Bunch love stuff like Haskell. Sone, esp with embedded focus, stay on C with a subset on Ada or embedded Java. The ones about oroving properties mostly do HOL, Coq, and ACL2. There’s also agent-oriented, term-rewriting, flow-based, logic-based… list goes on.
You might think it’s all about types because you’re on forums whose users mostly submit that stuff or similarly next to Universities that focus on it.