John C. Reynolds
John C. Reynolds | |
|---|---|
 | |
| Born | John Charles Reynolds June 1, 1935 United States |
| Died | April 28, 2013 (aged 77) |
| Education | Purdue University Ph.D., Harvard University (1961) |
| Known for | continuations, definitional interpreters, defunctionalization, Forsythe, Gedanken language, intersection types, polymorphic lambda calculus, relational parametricity, separation logic, ALGOL |
| Awards | Lovelace Medal (2010) |
| Scientific career | |
| Fields | Computer scientist |
| Institutions | Syracuse University Carnegie Mellon University |
| Thesis | Surface Properties of Nuclear Matter (1961) |
| Doctoral students | Benjamin C. Pierce |
| Website | www |
John Charles Reynolds (June 1, 1935 – April 28, 2013) was an American computer scientist.[1]
Education and affiliations
[edit]John Reynolds studied at Purdue University and then earned a Doctor of Philosophy (Ph.D.) in theoretical physics from Harvard University in 1961. He was a professor of information science at Syracuse University from 1970 to 1986. From then until his death, he was a professor of computer science at Carnegie Mellon University. He also held visiting positions at Aarhus University (Denmark), The University of Edinburgh, Imperial College London, Microsoft Research (Cambridge, UK) and Queen Mary University of London.
Academic work
[edit]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.[2]
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
[edit]- Books
- The Craft of Programming, Prentice Hall International, 1981. ISBN 0-13-188862-5.
- Theories of Programming Languages, Cambridge University Press, 1998. ISBN 0-521-59414-6.
- Articles
- "Transformational Systems and the Algebraic Structure of Atomic Formulas" (PDF). Machine Intelligence. 5: 135–151. 1970.
- "Towards a Theory of Type Structure" (PDF). Colloque sur la Programmation. Paris, France. 1974. pp. 408–425. doi:10.1007/3-540-06859-7_148. Retrieved 2014-11-06.
- "Types, Abstraction and Parametric Polymorphism" (PDF). Information Processing '83. 1983. pp. 513–523. Archived from the original (PDF) on 2016-03-10. Retrieved 2014-11-06.
- "Separation Logic: A Logic for Shared Mutable Data Structures" (PDF). 17th IEEE Symposium on Logic in Computer Science (LICS 2002). pp. 55–74. doi:10.1109/LICS.2002.1029817.
References
[edit]- ^ Fisher, Larry (29 April 2013). "John Reynolds, 1935–2013". Communications of the ACM: ACM News. United States: Association for Computing Machinery. Retrieved 30 April 2013.
- ^ O'Hearn, Peter; Tennent, Robert D. (1997). Algol-Like Languages. Cambridge, Massachusetts, United States: Birkhauser Boston. doi:10.1007/978-1-4612-4118-8. ISBN 978-0-8176-3880-1. S2CID 6273486.
Further reading
[edit]- Olivier Danvy, Peter O'Hearn and Philip Wadler (editors), "Festschrift for John C. Reynolds's 70th Birthday Archived 2012-07-03 at the Wayback Machine". Theoretical Computer Science, 375(1–3):1–350, 1 May 2007. Editorial, pages 1–2. doi:10.1016/j.tcs.2006.12.024
- Stephen Brookes, Peter O'Hearn and Uday Reddy, "The Essence of Reynolds". POPL 2014, pages 251–256. doi:10.1145/2535838.2537851
External links
[edit]- Official website
- Curriculum Vitae
- John C. Reynolds at DBLP Bibliography Server
- John C. Reynolds at the Mathematics Genealogy Project
- Program Verification and Semantics: Further Work (London, 2004)
- 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