[TYPES] history of typing contexts

[Andrew Pitts]

When formulating a type theory there are (at least) two different
approaches to how variables are typed:

- variables come tagged with an explicit type

- variables are assigned types in a typing context that forms part of
the typing judgement

I believe that the first approach can be traced back to Church's
original 1940 paper on the Simple Theory of Types. Can any one tell me
about the origins of the second approach?

Andy Pitts