29 May
2001
29 May
'01
10:44 a.m.
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ón