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.