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

computer scientist A computer scientist is a person who is trained in the academic study of computer science. Computer scientists typically work on the theoretical side of computation, as opposed to the hardware side on which computer engineers mainly focus (al ...

Education and affiliations

John Reynolds studied at Purdue University and then earned a

Doctor of Philosophy A Doctor of Philosophy (PhD, Ph.D., or DPhil; Latin: or ') is the most common degree at the highest academic level awarded following a course of study. PhDs are awarded for programs across the whole breadth of academic fields. Because it is ...

(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 natural phenomena. This is in contrast to experimental physics, which uses experi ...

from

Harvard University Harvard University is a private Ivy League research university in Cambridge, Massachusetts. Founded in 1636 as Harvard College and named for its first benefactor, the Puritan clergyman John Harvard, it is the oldest institution of high ...

in 1961. He was a professor of

information science Information science (also known as information studies) is an academic field which is primarily concerned with analysis, collection, classification, manipulation, storage, retrieval, movement, dissemination, and protection of information. ...

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

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

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

Carnegie Mellon University Carnegie Mellon University (CMU) is a private research university in Pittsburgh, Pennsylvania. One of its predecessors was established in 1900 by Andrew Carnegie as the Carnegie Technical Schools; it became the Carnegie Institute of Technology ...

. He also held visiting positions at

Aarhus University Aarhus University ( da, Aarhus Universitet, abbreviated AU) is a public research university with its main campus located in Aarhus, Denmark. It is the second largest and second oldest university in Denmark. The university is part of the Coimbra G ...

(

Denmark ) , song = ( en, "King Christian stood by the lofty mast") , song_type = National and royal anthem , image_map = EU-Denmark.svg , map_caption = , subdivision_type = Sovereign state , subdivision_name = Kingdom of Denmark , establishe ...

University of Edinburgh The University of Edinburgh ( sco, University o Edinburgh, gd, Oilthigh Dhùn Èideann; abbreviated as ''Edin.'' in post-nominals) is a public research university based in Edinburgh, Scotland. Granted a royal charter by King James VI in 15 ...

Imperial College London Imperial College London (legally Imperial College of Science, Technology and Medicine) is a public research university in London, United Kingdom. Its history began with Prince Albert, consort of Queen Victoria, who developed his vision for a ...

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 university city and the county town in Cambridgeshire, England. It is located on the River Cam approximately north of London. As of the 2021 United Kingdom census, the population of Cambridge was 145,700. Cambridge beca ...

, UK) and

Queen Mary University of London Queen Mary University of London (QMUL, or informally QM, and previously 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 of ...

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. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language. The description of a programming l ...

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 executa ...

s, especially concerning formal

semantics Semantics (from grc, σημαντικός ''sēmantikós'', "significant") is the study of reference, meaning, or truth. The term can be used to refer to subfields of several distinct disciplines, including philosophy, linguistics and compu ...

. He invented the

polymorphic lambda calculus System F (also polymorphic lambda calculus or second-order lambda calculus) is a typed lambda calculus that introduces, to simply typed lambda calculus, a mechanism of universal quantification over types. System F formalizes parametric polymorphis ...

(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 exa ...

; 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 the research director (emeritus) at the mathematical institute of the University of Aix-Marseille, at Luminy. Biography Jean-Yves Girard is an alumnus of th ...

. 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 to programming language

. He defined the programming languages Gedanken and Forsythe, known for its use of

intersection type In type theory, an intersection type can be allocated to values that can be assigned both the type \sigma and the type \tau. This value can be given the intersection type \sigma \cap \tau in an intersection type system. Generally, if the ranges o ...

s. 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 assertion ...

to describe and reason about shared mutable

data structure In computer science, a data structure is a data organization, management, 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 rel ...

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 th ...

, 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 f ...

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 f ...

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) is a typed functional language introduced by Gordon Plotkin in 1977, based on previous unpublished material by Dana Scott. It can be considered to be an extended version of the typed la ...

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

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

'' and the ''

Journal of the ACM The ''Journal of the ACM'' 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 An editor-in-c ...

''. 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 member ...

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

Lovelace Medal The Lovelace Medal was established by the British Computer Society 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 UK. Award ...

from the

British Computer Society Sir Maurice Wilkes served as the first President of BCS in 1957 BCS, The Chartered Institute for IT, known as the British Computer Society until 2009, is a professional body and a learned society that represents those working in infor ...

in 2010.

Selected publications

;Books
''The Craft of Programming''

Prentice Hall Prentice Hall was an American major educational publisher owned by Savvas Learning Company. Prentice Hall publishes print and digital content for the 6–12 and higher-education market, and distributes its technical titles through the Safari B ...

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

Cambridge University Press Cambridge University Press is the university press of the University of Cambridge. Granted letters patent by Henry VIII of England, King Henry VIII in 1534, it is the oldest university press in the world. It is also the King's Printer. Cambr ...

, 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 Academic journal editors Microsoft employees Fellows of the Association for Computing Machinery

Education and affiliations

Academic work

Selected publications

References

Further reading

External links