Reynolds's main research interest was in the area of
programming language design and associated
specification languages, especially concerning formal
semantics. He invented the
polymorphic lambda calculus (System F) and formulated the property of semantic
parametricity; the same calculus was independently discovered by
Jean-Yves Girard. He wrote a seminal paper on definitional interpreters, which clarified early work on
continuations and introduced the technique of
defunctionalization. He applied
category theory to programming language
semantics. He defined the programming languages Gedanken and Forsythe, known for their use of
intersection types. He worked on a
separation logic to describe and reason about shared mutable
data structures. Reynolds created an elegant, idealized formulation of the programming language
ALGOL, which exhibits ALGOL's syntactic and semantic purity, and is used in programming language research. It also made a convincing methodologic argument regarding the suitability of local effects in the context of
call-by-name languages, in contrast with the global effects used by
call-by-value languages such as
ML. The conceptual integrity of the language made it one of the main objects of semantic research, along with
Programming Computable Functions (PCF) and ML. He was an editor of journals such as the
Communications of the ACM and the
Journal of the ACM. In 2001, he was appointed a Fellow of the
Association for Computing Machinery (ACM). He won the
ACM SIGPLAN Programming Language Achievement Award in 2003, and the
Lovelace Medal from the
British Computer Society in 2010. ==Selected publications==