John Reynolds, 1935 – 2013

John C. Reynolds, a professor of computer science at Carnegie Mellon University (CMU), died April 28 following a heart attack.

Reynolds received his Ph.D. in theoretical physics from Harvard University in 1961. While working at Argonne National Laboratory, he came to realize that his passion was for computation, according to Randy Bryant, dean of the School of Computer Science and University Professor of Computer Science at CMU, who said that, as a result, Reynolds "became a very successful computer scientist, focusing on the logical foundations of programs and programming languages." He served as a professor of Information Science at Syracuse University from 1970 to 1986 and then joined CMU as a member of the faculty of the Computer Science Department (CSD). He retired in 2012, but continued to serve CSD as professor emeritus.

He also had held visiting positions at Aarhus University (Denmark), University of Edinburgh, Imperial College London, Microsoft Research (Cambridge), and Queen Mary, University of London (UK).

According to his CSD homepage, Reynolds’research focused "on the design of programming languages and languages for specifying program behavior, mathematical tools for defining the semantics of such languages, and methods for proving that programs meet their specifications." A secondary area of interest was "the semantics of types. The last 15 years have seen the discovery of a variety of type systems that have vastly enlarged our notions of what types are and how they might be used. My goal is to understand the meaning of these systems and to find a general concept of type of which they are all instances."

In addition, Reynolds was interested "in the design, definition, and proof methodology of Algol-like languages, which combine imperative constructs with a powerful procedure mechanism, while retaining the concepts of block structure and local variables."

Robert Harper, also a computer science professor in CSD, described Reynolds as "a mentor and an inspiration for many of us, providing a fine example of what it means to be scientist, a scholar, and a gentleman. John’s meticulous attention to detail and uncompromising insistence on excellence exemplifies the very best qualities of a scientist that we all seek to emulate." In a 2010 letter nominating Reynolds for the Japan Prize, Harper wrote, "The profound influence of Reynolds’ work in academic computer science is now being felt in the computer industry. The concept of generic types in the Java and C# programming languages originates in Reynolds’ 1978 paper on the polymorphic λ-calculus. Verification tools for imperative programs are now used widely in the software industry, drawing heavily on Reynolds’s work on program specification and verification, in particular the sharply original concept of separation logic, which permits modular verification of large software systems by controlling interference among its components."

CMU’s Bryant said, "John has made many important contributions over his career. Interestingly, his 2002 work on separation logic, done jointly with Peter O’Hearn and others, has been especially prominent. Separation logic provides a formal way to reason about what we might think of as ‘normal programs,’ i.e., ones that operate by changing the values stored in memory, but where memory is partitioned into independent blocks, and so we can reason about different program components independently. I can only hope that the work I do at age 67 would be counted among my best."

Reynolds had been on the editorial boards of journals such as the Communications of the ACM and the Journal of the ACM. In 2001, he was appointed a Fellow of the ACM. He received the ACM SIGPLAN Programming Language Achievement Award in 2003, and the Lovelace Medal from the British Computer Society in 2010.

Added Bryant, "We will also remember John for this cheerful spirit, his high ethical standards, and his deep intellect. He will very much be missed."