John C. Reynolds
Encyclopedia
United States
The United States of America is a federal constitutional republic comprising fifty states and a federal district...
computer scientist
Computer scientist
A computer scientist is a scientist who has acquired knowledge of computer science, the study of the theoretical foundations of information and computation and their application in computer systems....
.
John Reynolds studied at Purdue University
Purdue University
Purdue University, located in West Lafayette, Indiana, U.S., is the flagship university of the six-campus Purdue University system. Purdue was founded on May 6, 1869, as a land-grant university when the Indiana General Assembly, taking advantage of the Morrill Act, accepted a donation of land and...
and then earned a PhD
PHD
PHD may refer to:*Ph.D., a doctorate of philosophy*Ph.D. , a 1980s British group*PHD finger, a protein sequence*PHD Mountain Software, an outdoor clothing and equipment company*PhD Docbook renderer, an XML renderer...
in theoretical physics
Theoretical physics
Theoretical physics is a branch of physics which employs mathematical models and abstractions of physics to rationalize, explain and predict natural phenomena...
from Harvard University
Harvard University
Harvard University is a private Ivy League university located in Cambridge, Massachusetts, United States, established in 1636 by the Massachusetts legislature. Harvard is the oldest institution of higher learning in the United States and the first corporation chartered in the country...
in 1961. He was Professor of Information science
Information science
-Introduction:Information science is an interdisciplinary science primarily concerned with the analysis, collection, classification, manipulation, storage, retrieval and dissemination of information...
at Syracuse University
Syracuse University
Syracuse University is a private research university located in Syracuse, New York, United States. Its roots can be traced back to Genesee Wesleyan Seminary, founded by the Methodist Episcopal Church in 1832, which also later founded Genesee College...
from 1970 to 1986. Since then he has been Professor of Computer Science
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
at Carnegie Mellon University
Carnegie Mellon University
Carnegie Mellon University is a private research university in Pittsburgh, Pennsylvania, United States....
. He has held visiting positions at Aarhus University (Denmark
Denmark
Denmark is a Scandinavian country in Northern Europe. The countries of Denmark and Greenland, as well as the Faroe Islands, constitute the Kingdom of Denmark . It is the southernmost of the Nordic countries, southwest of Sweden and south of Norway, and bordered to the south by Germany. Denmark...
), University of Edinburgh
University of Edinburgh
The University of Edinburgh, founded in 1583, is a public research university located in Edinburgh, the capital of Scotland, and a UNESCO World Heritage Site. The university is deeply embedded in the fabric of the city, with many of the buildings in the historic Old Town belonging to the university...
, Imperial College London
Imperial College London
Imperial College London is a public research university located in London, United Kingdom, specialising in science, engineering, business and medicine...
,
Microsoft Research
Microsoft Research
Microsoft Research is the research division of Microsoft created in 1991 for developing various computer science ideas and integrating them into Microsoft products. It currently employs Turing Award winners C.A.R. Hoare, Butler Lampson, and Charles P...
(Cambridge
Cambridge
The city of Cambridge is a university town and the administrative centre of the county of Cambridgeshire, England. It lies in East Anglia about north of London. Cambridge is at the heart of the high-technology centre known as Silicon Fen – a play on Silicon Valley and the fens surrounding the...
) and Queen Mary, University of London
Queen Mary, University of London
Queen Mary, University of London is a public research university located in London, United Kingdom and a constituent college of the federal University of London...
(UK
United Kingdom
The United Kingdom of Great Britain and Northern IrelandIn the United Kingdom and Dependencies, other languages have been officially recognised as legitimate autochthonous languages under the European Charter for Regional or Minority Languages...
).
Reynolds's main research interest is in the area of programming language
Programming language
A programming language is an artificial language designed to communicate instructions to a machine, particularly a computer. Programming languages can be used to create programs that control the behavior of a machine and/or to express algorithms precisely....
design and associated specification language
Specification language
A specification language is a formal language used in computer science.Unlike most programming languages, which are directly executable formal languages used to implement a system, specification languages are used during systems analysis, requirements analysis and systems design.Specification...
s, especially concerning formal semantics
Semantics
Semantics is the study of meaning. It focuses on the relation between signifiers, such as words, phrases, signs and symbols, and what they stand for, their denotata....
. He invented the Polymorphic Lambda Calculus and formulated the property of semantic parametricity
Parametricity
Parametricity is a result in the theory of programming languages in computer science. The principle of parametricity dictates that functions with similar types have similar properties.- Theory of parametricity :...
; the same calculus was independently discovered by Jean-Yves Girard
Jean-Yves Girard
Jean-Yves Girard is a French logician working in proof theory. His contributions include a proof of strong normalization in a system of second-order logic called system F; the invention of linear logic; the geometry of interaction; and ludics...
. He wrote a seminal paper on definitional interpreters, which clarified early work on continuations and introduced the technique of defunctionalization
Defunctionalization
In programming languages, defunctionalization refers to 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 paper, "Definitional Interpreters for Higher-Order...
. He defined the programming languages Gedanken and Forsythe. He has worked on a separation logic
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 Burstall...
to describe and reason about shared mutable data structure
Data structure
In computer science, a data structure is a particular way of storing and organizing data in a computer so that it can be used efficiently.Different kinds of data structures are suited to different kinds of applications, and some are highly specialized to specific tasks...
s.
He has been an editor of journals such as the Communications of the ACM
Communications of the ACM
Communications of the ACM is the flagship monthly journal of the Association for Computing Machinery . First published in 1957, CACM is sent to all ACM members, currently numbering about 80,000. The articles are intended for readers with backgrounds in all areas of computer science and information...
and the Journal of the ACM
Journal of the ACM
The Journal of the ACM is the flagship scientific journal of the Association for Computing Machinery . It is peer-reviewed and covers computer science in general, especially theoretical aspects. Its current editor-in-chief is Victor Vianu, from University of California, San Diego.The journal has...
. In 2001, he was appointed a Fellow of the ACM
Association for Computing Machinery
The Association for Computing Machinery is a learned society for computing. It was founded in 1947 as the world's first scientific and educational computing society. Its membership is more than 92,000 as of 2009...
. He won the ACM SIGPLAN Programming Language Achievement Award in 2003.
Books
- Theories of Programming Languages, Cambridge University PressCambridge University PressCambridge University Press is the publishing business of the University of Cambridge. Granted letters patent by Henry VIII in 1534, it is the world's oldest publishing house, and the second largest university press in the world...
, 1998. ISBN 0-521-59414-6 - The Craft of Programming, Prentice HallPrentice HallPrentice Hall is a major educational publisher. It is an imprint of Pearson Education, Inc., based in Upper Saddle River, New Jersey, USA. Prentice Hall publishes print and digital content for the 6-12 and higher-education market. Prentice Hall distributes its technical titles through the Safari...
International, 1981. ISBN 0-13-188862-5
External links
- Home page
- Curriculum Vitae (PostScriptPostScriptPostScript is a dynamically typed concatenative programming language created by John Warnock and Charles Geschke in 1982. It is best known for its use as a page description language in the electronic and desktop publishing areas. Adobe PostScript 3 is also the worldwide printing and imaging...
format) - DBLP publications
- Festschrift for his 70th birthday, edited by Olivier DanvyOlivier DanvyOlivier Danvy is a French computer scientist specializing in programming languages, partial evaluation, and continuations at the University of Aarhus in Denmark.He is notable for the number of scientific papers which acknowledge his help...
, Peter O'HearnPeter O'HearnPeter William O'Hearn is a computer scientist based in the United Kingdom.Peter O'Hearn attained a BSc degree in Computer Science from Dalhousie University, Halifax, Nova Scotia , followed by MSc and PhD degrees fromQueen's University, Kingston, Ontario, Canada...
and Philip WadlerPhilip WadlerPhilip Wadler is a computer scientist known for his contributions to programming language design and type theory. In particular, he has contributed to the theory behind functional programming and the use of monads in functional programming, the design of the purely functional language Haskell, and... - Program Verification and Semantics: Further Work (London, 2004)