John Charles Reynolds (June 1, 1935 – April 28, 2013) was an American

computer scientist A computer scientist is a scientist who specializes in the academic study of computer science. Computer scientists typically work on the theoretical side of computation. Although computer scientists can also focus their work and research on ...

Education and affiliations

John Reynolds studied at

Purdue University Purdue University is a Public university#United States, public Land-grant university, land-grant research university in West Lafayette, Indiana, United States, and the flagship campus of the Purdue University system. The university was founded ...

and then earned a

Doctor of Philosophy A Doctor of Philosophy (PhD, DPhil; or ) is a terminal degree that usually denotes the highest level of academic achievement in a given discipline and is awarded following a course of Postgraduate education, graduate study and original resear ...

(Ph.D.) in

theoretical physics Theoretical physics is a branch of physics that employs mathematical models and abstractions of physical objects and systems to rationalize, explain, and predict List of natural phenomena, natural phenomena. This is in contrast to experimental p ...

from

Harvard University Harvard University is a Private university, private Ivy League research university in Cambridge, Massachusetts, United States. Founded in 1636 and named for its first benefactor, the History of the Puritans in North America, Puritan clergyma ...

in 1961. He was a professor of information science at

Syracuse University Syracuse University (informally 'Cuse or SU) is a Private university, private research university in Syracuse, New York, United States. It was established in 1870 with roots in the Methodist Episcopal Church but has been nonsectarian since 1920 ...

from 1970 to 1986. From then until his death, he was a professor of

computer science Computer science is the study of computation, information, and automation. Computer science spans Theoretical computer science, theoretical disciplines (such as algorithms, theory of computation, and information theory) to Applied science, ...

Carnegie Mellon University Carnegie Mellon University (CMU) is a private research university in Pittsburgh, Pennsylvania, United States. The institution was established in 1900 by Andrew Carnegie as the Carnegie Technical Schools. In 1912, it became the Carnegie Institu ...

. He also held visiting positions at

Aarhus University Aarhus University (, abbreviated AU) is a public research university. Its main campus is located in Aarhus, Denmark. It is the second largest and second oldest university in Denmark. The university is part of the Coimbra Group, the Guild, and Ut ...

(

Denmark Denmark is a Nordic countries, Nordic country in Northern Europe. It is the metropole and most populous constituent of the Kingdom of Denmark,, . also known as the Danish Realm, a constitutionally unitary state that includes the Autonomous a ...

The University of Edinburgh The University of Edinburgh (, ; abbreviated as ''Edin.'' in Post-nominal letters, post-nominals) is a Public university, public research university based in Edinburgh, Scotland. Founded by the City of Edinburgh Council, town council under th ...

Imperial College London Imperial College London, also known as Imperial, is a Public university, public research university in London, England. Its history began with Prince Albert of Saxe-Coburg and Gotha, Prince Albert, husband of Queen Victoria, who envisioned a Al ...

Microsoft Research Microsoft Research (MSR) is the research subsidiary of Microsoft. It was created in 1991 by Richard Rashid, Bill Gates and Nathan Myhrvold with the intent to advance state-of-the-art computing and solve difficult world problems through technologi ...

(

Cambridge Cambridge ( ) is a List of cities in the United Kingdom, city and non-metropolitan district in the county of Cambridgeshire, England. It is the county town of Cambridgeshire and is located on the River Cam, north of London. As of the 2021 Unit ...

, UK) and

Queen Mary University of London Queen Mary University of London (QMUL, or informally QM, and formerly Queen Mary and Westfield College) is a public university, public research university in Mile End, East London, England. It is a member institution of the federal University ...

Academic work

Reynolds's main research interest was in the area of

programming language A programming language is a system of notation for writing computer programs. Programming languages are described in terms of their Syntax (programming languages), syntax (form) and semantics (computer science), semantics (meaning), usually def ...

design and associated

specification language A specification language is a formal language in computer science used during systems analysis, requirements analysis, and systems design to describe a system at a much higher level than a programming language, which is used to produce the exec ...

s, especially concerning formal

semantics Semantics is the study of linguistic Meaning (philosophy), meaning. It examines what meaning is, how words get their meaning, and how the meaning of a complex expression depends on its parts. Part of this process involves the distinction betwee ...

. He invented the polymorphic lambda calculus (System F) and formulated the property of semantic

parametricity In programming language theory, parametricity is an abstract uniformity property enjoyed by parametrically polymorphic functions, which captures the intuition that all instances of a polymorphic function act the same way. Idea Consider this ex ...

; the same calculus was independently discovered by

Jean-Yves Girard Jean-Yves Girard (; born 1947) is a French logician working in proof theory. He is a research director (emeritus) at the mathematical institute of University of Aix-Marseille, at Luminy. Biography Jean-Yves Girard is an alumnus of the Éc ...

. He wrote a seminal paper on definitional interpreters, which clarified early work on

continuation In computer science, a continuation is an abstract representation of the control state of a computer program. A continuation implements ( reifies) the program control state, i.e. the continuation is a data structure that represents the computat ...

s and introduced the technique of

defunctionalization In programming languages, defunctionalization is a compile-time transformation which eliminates higher-order functions, replacing them by a single first-order ''apply'' function. The technique was first described by John C. Reynolds in his 1972 pa ...

. He applied

category theory Category theory is a general theory of mathematical structures and their relations. It was introduced by Samuel Eilenberg and Saunders Mac Lane in the middle of the 20th century in their foundational work on algebraic topology. Category theory ...

to programming language

. He defined the programming languages Gedanken and Forsythe, known for their use of intersection types. He worked on a

separation logic In computer science, separation logic is an extension of Hoare logic, a way of reasoning about programs. It was developed by John C. Reynolds, Peter O'Hearn, Samin Ishtiaq and Hongseok Yang, drawing upon early work by Rod Burstall. The assertio ...

to describe and reason about shared mutable

data structure In computer science, a data structure is a data organization and storage format that is usually chosen for Efficiency, efficient Data access, access to data. More precisely, a data structure is a collection of data values, the relationships amo ...

s. Reynolds created an elegant, idealized formulation of the programming language

ALGOL ALGOL (; short for "Algorithmic Language") is a family of imperative computer programming languages originally developed in 1958. ALGOL heavily influenced many other languages and was the standard method for algorithm description used by the ...

, 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 In a programming language, an evaluation strategy is a set of rules for evaluating expressions. The term is often used to refer to the more specific notion of a ''parameter-passing strategy'' that defines the kind of value that is passed to the ...

languages, in contrast with the global effects used by

call-by-value In a programming language, an evaluation strategy is a set of rules for evaluating expressions. The term is often used to refer to the more specific notion of a ''parameter-passing strategy'' that defines the kind of value that is passed to the ...

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 In computer science, Programming Computable Functions (PCF), or Programming with Computable Functions, or Programming language for Computable Functions, is a programming language which is typed and based on functional programming, introduced by G ...

(PCF) and ML. He was an editor of journals such as the ''

Communications of the ACM ''Communications of the ACM'' (''CACM'') is the monthly journal of the Association for Computing Machinery (ACM). History It was established in 1958, with Saul Rosen as its first managing editor. It is sent to all ACM members. Articles are i ...

'' and the ''

Journal of the ACM The ''Journal of the ACM'' (''JACM'') is a peer-reviewed scientific journal covering computer science in general, especially theoretical aspects. It is an official journal of the Association for Computing Machinery. Its current editor-in-chief is ...

''. In 2001, he was appointed a Fellow of the

Association for Computing Machinery The Association for Computing Machinery (ACM) is a US-based international learned society for computing. It was founded in 1947 and is the world's largest scientific and educational computing society. The ACM is a non-profit professional membe ...

(ACM). He won the ACM SIGPLAN Programming Language Achievement Award in 2003, and the

Lovelace Medal The Lovelace Medal was established by BCS, The Chartered Institute for IT in 1998, and is presented to individuals who have made outstanding contributions to the understanding or advancement of computing. It is the top award in computing in the U ...

from the

British Computer Society image:Maurice Vincent Wilkes 1980 (3).jpg, Sir Maurice Wilkes served as the first President of BCS in 1957. The British Computer Society (BCS), branded BCS, The Chartered Institute for IT, since 2009, is a professional body and a learned ...

in 2010.

Selected publications

;Books
''The Craft of Programming''

Prentice Hall Prentice Hall was a major American publishing#Textbook_publishing, educational publisher. It published print and digital content for the 6–12 and higher-education market. It was an independent company throughout the bulk of the twentieth cen ...

International, 1981. . * ''Theories of Programming Languages'',

Cambridge University Press Cambridge University Press was the university press of the University of Cambridge. Granted a letters patent by King Henry VIII in 1534, it was the oldest university press in the world. Cambridge University Press merged with Cambridge Assessme ...

, 1998. . ;Articles * * * *

References

External links

*
Curriculum Vitae
* *
Program Verification and Semantics: Further Work
(London, 2004) {{DEFAULTSORT:Reynolds, John C. 1935 births 2013 deaths Harvard University alumni Purdue University alumni American computer scientists Formal methods people Programming language researchers Academics of Imperial College London Academics of Queen Mary University of London Academics of the University of Edinburgh Syracuse University faculty Carnegie Mellon University faculty American academic journal editors Microsoft employees 2001 fellows of the Association for Computing Machinery

Education and affiliations

Academic work

Selected publications

References

Further reading

External links