First-hand anecodote on the naming of the pi-calculus, courtesy of John Power. Robin Milner viewed it as a successor to the lambda calculus. What comes after lambda in the greek alphabet? Mu, but there was already a mu-calculus. Nu comes next, but sounds too similiar to mu. Next up is omicron, but who’d want to work on the “omicron calculus”?! And so you get to pi. PI CALCULUS.
Gérard Huet’s opening talk was amazing. He talked flowingly for 40 minutes, entirely from memory. He talked about the early days of ML, including the ‘split’ between Standard ML and the INRIA caml/caml-light/ocaml. He described being asked by Milner to rename the INRIA flavour of ML after the Standard ML effort, and then cheekily naming it CAML, ostensibly because of the Categorical Abstract Machine but usefully keeping ML in the name.
I really enjoyed Xavier Leroy’s talk about a future in which programming languages and theorem provers increasingly blend into one – an area which I keep meaning to get deeper into. I also thought Benjamin Pierce’s talk was really appropriate for the occasion – taking the time to walk through the Hindley-Milner (or Milner, or Damas-Hindley-Milner) type inference algorithm in detail.