POPL Invited talks

POPL was the main conference running during the week. It ran from Wednesday to
Friday with 2 streams.

There were three invited talks, the first was an award, speech and interview.
I forget the name of the award but the purpose was to recognize a paper 40
years after it's publication based on that paper's impact in the last 40 years.
The recipient was Sir Charles Antony Richard Hoare for his paper An axiomatic
basis for computer programming. I'm sad to say that I wasn't aware of Sir
Hoare before POPL; now I'm very interested to read a few of his papers. The
interview referred to several of his papers during his career, and if I'm not
mistaken the interviewer was one of his students.

The second invited talk was given by Jennifer Rexford; this is probably the
invited talk that spoke the most to me. Jennifer had seen a problem in network
administration and operations. The problem is that each router has it's own
configuration and that this is fine if the network has a single router. But
once there are two or more routers the configurations have to agree about
certain things, and that the software that coordinates large networks doesn't
always do a good job - let alone ensure that the configurations are consistent.
Jenifier wrote a domain specific language to solve this problem. I like this
because it's a problem that many people have, and the solution is
straightforward (at least on the surface). And by providing such a solution
her work has a large impact.

The third invited talk was also very good. J Strother Moore demonstrated a
theorem prover. Moore is the same Moore as in the Boyer-Moore string search
algorithm, a very influential researcher. Theorem provers are increasing in
popularity. I felt like the only person in the room who hadn't used one (let
alone written one). So, for me it was good to see this used and demonstrated
in front of my eyes. The anecdotes of this talk where also very interesting;
for instance, AMD used Moore's theorem prover to check the soundness of
floating point division in the K5, after Intel were dealing with the famous
floating point division bug in the newly released Pentium.
(AMD have continued to use the theorem prover).

I still have more notes to write up.