Abstract

Looking at late John Reynolds's long and illustrious career, we see a dramatic shift in his research output marked by the publication of the programming text book, "Craft of Programming". Gone are domain theory and low-level implementation issues from his repertoire. Instead, he published a series of landmark papers of greater generality in quick succession. Category-theoretic type conversions in 1980, The Essence of Algol in 1981, Specification Logic in 1982, and Types, Abstraction and Parametric Polymorphism in 1983. Did the "Craft of Programming" transform Reynolds?

I would like to propose that there are deep and intriguing connections between programming languages and category-theoretic mathematics. Exploring these connections is likely to enrich both the disciplines. In particular, programming languages involve an interplay between the intensional and extensional views of functions, which is also at work in all axiomatic theories in mathematics. The "Craft of Programming" unearths these connections, and poses a deep question: if the present day category theory is unable to capture the abstractions involved in programming, what is it missing? Answering this question is rightly called the "Reynolds programme".