Billy Goats Gruff

In 2009 Ruy de Queiroz first asked his logician friends, me included, about Rolf Schock Prize nominations.

I think it's very nice that Ruy gets asked this kind of question. So I tried to help in 2009 with a tale of Bills.

I'd like to nominate Three Bills: William A. Howard, William W. Tait and F. William Lavwere. No, it's not a kid's story, even if the three Billy Goats Gruff come to mind. The reason I think this is a sensible nomination is that the three are involved in the project that came to be known as the Curry-Howard Correspondence. The Curry-Howard correspondence is one of the big forces behind the advancement of logic and philosophy as   engines of Computer Science in the last fifty years.

The Curry-Howard correspondence asserts that propositions in (certain systems of) logic correspond to types in (certain kinds of) programming languages, that proofs in those logics correspond to terms in the these programming languages and that simplification of proofs correspond to computation in the related  languages. As can be easily seen even in this oversimplified description, the correspondence has far-reaching consequences for both logic and programming. In particular it allows for results in either area to be exploit in the other--a hallmark of a deep result in Mathematics.

Howard is already, together with H. Curry named in the the correspondence, which wouldn't have the impact it has without the work of Tait and Lawvere. Tait is responsible to the part of the correspondence that relates proof simplification to computation, possibly the most important component of the correspondence. And Lawvere (together with Lambek and many other category theorists) is the one that made it all beautiful mathematics, by relating it to the Theory of Categories. Lawvere showed in his thesis (1968) that the correspondence could be  extended to (special classes of) categories and that, once again, results in pure category theory correspond to logical (and hence also programming) results, so that one can work in whichever field there are tools available and then transfer the results to the other fields. It's remarkable and very beautiful, albeit still hard to explain without the full mathematical apparatus.

Nonetheless given the Rolf's prize interest in making sure that society in general is aware of the importance of philosophy  and logic matters for humanity, and given the importance of computing and its understanding for society as a whole, the nomination of the three Bills seems to me a sensible option.