> > > 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! However, I'd suggest looking at Michael Schwartzbach's lecture notes on Polymorphic Type Inference, which are on the web at http://www.daimi.aau.dk/~mis/typeinf.ps The typing rule notation is explained in the first couple of pages, and then used to explain many variants on type systems, show how inference works, etc. I have a collection of links to such articles at http://www.md.chalmers.se/~rjmh/tutorials.html which you might find useful. John Hughes