Notation question

[Jon Fairbairn]

> and not just type systems but also other aspects of operational
> semantics. What we have here is a single rule from a rule-based
> inductive definition of a certain relation G |- s :: S between typing
> environments G, expressions s and types S.

It's probably worth mentioning here that this notation
originated (I think) in mathematical logic, as a way of
presenting formal systems. Try "Gentzen", "Natural
Deduction" and "Sequent Calculus" as search terms.

  J=F3n