A Reynolds Programme for Category Theory and Programming Languages

**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".