Two early papers

I've added links to two important early papers on types to the course web page. The first paper is Church's 1940 paper on "A Formulation of the Simple Theory of Types", which introduces the simply typed lambda calculus. The second is Newman's 1942 paper on "Stratified Systems of Logic", which I got from Jean-Jacques Levy, who got it from Roger Hindley. This may be the first paper that describes a process that could be considered type checking.

If you download these papers and look at them, you'll see that the terminology and notation are rather antique and laborious by modern standards, and they refer to issues and systems that are no longer current, so reading them is a lot of work. But it is probably worthwhile spending a little time trying to reconstruct what is going on in comparison with our current ways of doing things (e.g. abstract syntax of terms). You will see that in those days they had a rather concrete view of syntax, lacking the notation of a grammar.