Notation question

[Andrew Pitts]

John Hughes said

> 	> > >  G |- f :: all x::S . T   G |- s :: S
> 	> > >--------------------------------------
> 	> > >          G |- f s :: [s/x]T
> 	>

> 	    Any more takers? I still don't have any pointers to literature where 
> 	this theorem notation is explained more fully, and I'd really like to have 
> 	some.

> This is a standard notation for describing type systems in articles on the
> subject -- so standard that it's hard to think of a good reference that
> actually explains it!

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. I seem to spend half my
life using such inductive definitions and the other half teaching them
to undergraduates (and the third half doing university administration,
hey ho). Casting modesty aside, to read about such things let me
recommend

<www.cl.cam.ac.uk/Teaching/2000/Semantics/> lecture notes on
operational semantics (esp section 2.3)

Andy Pitts