[tikhonj]

Eh. The first time I saw typing rules in class was in a moderately specialized graduate course, so it would have been very easy to get a perfectly good CS education without learning about them.

Of course, I go to a university that seems very biased towards practical engineering sorts of topics over theory, so your experience may vary.

[richardwhiuk]

In Univ of Cambridge CS course it's covered in second year undergraduate material - see http://www.cl.cam.ac.uk/teaching/1213/Types/ (though not referred to by name explicitly).

[TillE]

Yeah, CS programs vary. At a SUNY school about 8 years ago, my experience was that it veered slightly more towards the practical, at least to the extent that we spent relatively little time with complex mathematical notation as we learned CS concepts.

Except for basic stuff like set theory and Boolean logic, math was for the required math classes.

[Periodic]

If you take a class in compilers you should see these sorts of inference rules when talking about operational semantics. Though maybe it isn't as popular to use operational semantics anymore. It's very useful to define rules in this syntax when working on semantic analysis and code generation.

I didn't get the background really necessary to really understand the type-theory parts of this notation until I took a graduate course in programming language theory.

[tikhonj]

Yeah, at my school operational semantics was only covered in that same PL theory course. The undergraduate programming languages/compilers course never went into it, unfortunately.