[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.