> 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




_______________________________________________
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Reply via email to