In 1941 Alonso Church wrote the book which introduced the calculi of l conversion. Then the first functional language was invented by John McCarthy and his co-workers and this manual was the first which got some popularity.
In 1966 Peter Landin was the first to consider the l calculus as a metalanguage and here is his seminal paper, the next seven hundred programming languages. And here its worthwhile remembering the joke: why did he pick such an odd number? Well, in fact originally he wanted to write the next one hundred programming languages. But unfortunately, the editor at the time-at that time there were no text editors - so the editor misread his handwriting and did not read a one but read a seven. And so - here we have this odd number, which now has become part of the folklore in the functional programming community.
Then in 1966 C. Böhm also proposed an independent way of using l calculus as a language description language and the reason why today I am here probably is because of this paper. Because this was the seminal paper in Italy which introduced the studies on functional languages. So if today we have a course like the one we are starting it is because in 1966 C. Böhm was the first to realise the descriptive power of typed l calculus.
In 1978 Robert Milner introduced the first polymorphic typing discipline which he applied to the metalanguage of a proof assistant for the logic of computable functions which was the logic for reasoning on domains. Now the metalanguage of this proof assistant was what will be another topic of our course that is the functional language ML. Martin Löf was the first to spell out in detail the analogy that I illustrated earlier and in fact it is named partially after him.
In 1987 Plotkin together with two collaborators-one of whom is actually myself, were the first to formulate the notion of a logical framework which is of a generic logic which could capture uniformities in the sense that we have explained earlier.
Then in 1988 we an extension of the typed-l calculus to the calculus of construction which became the specification language of the formal proof assistant that we are going to illustrate in this course that is the assistant Coq, which was actually implemented in a definite and usable form in 1993. And in 1990 we have the first complete formal definition of a truly usable programming language given by Milner and co-workers.
