I was long curious about how does λ calculus become the foundation of formalizaing programming languages. It’s strange that I haven’t look up the answer until today: It’s invented so early by Alonzo Church (whom I will write another post for) as an alternative mathematic foundation in 1930s and its relation with programming language was re-discoverred in 1960s.

From the “Lambda calculus and programming languages” section of wikipedia page:

As pointed out by Peter Landin’s 1965 paper “A Correspondence between ALGOL 60 and Church’s Lambda-notation”

I found this name quite familiar since I read his paper “The mechanical evaluation of expressions” before, in which he introduced the first abstract machine for functional programming language, namely SECD machine. This paper also define the term Closure) which becomes a prevalent notion in computer programming nowadays.

Besides of that, his contributions also include:

  • on ALGO definition
  • ISWIM programming language
  • off-side rule, known as “indentation-based” syntax nowadays, popularized by Miranda, Haskell, Python, etc.
  • coin the term syntactic sugar

He was much influenced by a study of McCarthy’s LISP and taught Tony Hoare ALGO with Peter Naur and Edsger W. Dijkstra. (Oh yes, definitely 4 more people to write).

I have just download his old, influential paper “The next 700 programming languages”.
I am sure it will be an enjoyable read.