Gordon Plotkin

Last updated

Gordon Plotkin

Gordon Plotkin.jpg
Plotkin in 2005
Born
Gordon David Plotkin

(1946-09-09) 9 September 1946 (age 77) [1]
Glasgow, Scotland
Alma mater University of Glasgow (BSc)
University of Edinburgh (PhD)
Known for Programming Computable Functions
Unbounded nondeterminism
Operational semantics
Domain theory
Awards
Scientific career
Fields Logic
Mathematics
Computer science
Institutions University of Edinburgh
Laboratory for Foundations of Computer Science
School of Informatics
University of Glasgow
Thesis Automatic methods of inductive inference  (1972)
Doctoral advisor
Doctoral students
Website homepages.inf.ed.ac.uk/gdp
inf.ed.ac.uk/people/staff/Gordon_Plotkin.html

Gordon David Plotkin, FRS FRSE MAE (born 9 September 1946) [1] is a theoretical computer scientist in the School of Informatics at the University of Edinburgh. Plotkin is probably best known for his introduction of structural operational semantics (SOS) and his work on denotational semantics. In particular, his notes on A Structural Approach to Operational Semantics were very influential. [9] [10] He has contributed to many other areas of computer science. [11] [12] [13] [14] [15] [16] [17]

Contents

Education

Plotkin was educated at the University of Glasgow and the University of Edinburgh, gaining his Bachelor of Science degree in 1967 [1] and PhD in 1972 [3] supervised by Rod Burstall. [2]

Career and research

Plotkin has remained at Edinburgh, and was, with Burstall and Robin Milner, a co-founder of the Laboratory for Foundations of Computer Science (LFCS). [18] [19] [20] [21] His former doctoral students include Luca Cardelli, [4] Philippa Gardner, [5] Doug Gurr, [6] Eugenio Moggi, [7] and Lǐ Wèi. [8] [2]

Awards and honours

Plotkin was elected a Fellow of the Royal Society (FRS) in 1992, and a Fellow of the Royal Society of Edinburgh (FRSE)[ when? ] and is a Member of the Academia Europæa [22] and the American Academy of Arts and Sciences. [23] He is also a winner of the Royal Society Wolfson Research Merit Award. Plotkin received the Milner Award in 2012 for "his fundamental research into programming semantics with lasting impact on both the principles and design of programming languages." [24] His nomination for the Royal Society reads:

Plotkin has contributed to Artificial Intelligence, Logic, Linguistics and especially to Computer Science. In AI he worked on hypothesis-formation and universal unification; in Logic, on frameworks for arbitrary logics; in Linguistics, on formalising situation theory. His main general contribution has been to establish a semantic framework for Computer Science, especially programming languages. Particular significant results are in the lambda-calculus (elementary models, definability, call-by-value), non-determinism (powerdomain theory), semantic formalisms (structured operational semantics, metalanguages), and categories of semantic domains (coherent, pro-finite, concrete). Further contributions concern the semantic paradigm of full abstraction, concurrency theory (event structures), programming logic and type theory. [25]

Related Research Articles

<span class="mw-page-title-main">Robin Milner</span> British computer scientist (1934–2010)

Arthur John Robin Gorell Milner was a British computer scientist, and a Turing Award winner.

Operational semantics is a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are verified by constructing proofs from logical statements about its execution and procedures, rather than by attaching mathematical meanings to its terms. Operational semantics are classified in two categories: structural operational semantics formally describe how the individual steps of a computation take place in a computer-based system; by opposition natural semantics describe how the overall results of the executions are obtained. Other approaches to providing a formal semantics of programming languages include axiomatic semantics and denotational semantics.

In programming language theory, semantics is the rigorous mathematical study of the meaning of programming languages. Semantics assigns computational meaning to valid strings in a programming language syntax. It is closely related to, and often crosses over with, the semantics of mathematical proofs.

<span class="mw-page-title-main">School of Informatics, University of Edinburgh</span>

The School of Informatics is an academic unit of the University of Edinburgh, in Scotland, responsible for research, teaching, outreach and commercialisation in informatics. It was created in 1998 from the former department of artificial intelligence, the Centre for Cognitive Science and the department of computer science, along with the Artificial Intelligence Applications Institute (AIAI) and the Human Communication Research Centre.

Patrick John Hayes FAAAI is a British computer scientist who lives and works in the United States. As of March 2006, he is a senior research scientist at the Institute for Human and Machine Cognition in Pensacola, Florida.

Matthew Hennessy is an Irish computer scientist who has contributed especially to concurrency, process calculi and programming language semantics.

<span class="mw-page-title-main">Programming language theory</span> Branch of computer science

Programming language theory (PLT) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of formal languages known as programming languages. Programming language theory is closely related to other fields including mathematics, software engineering, and linguistics. There are a number of academic conferences and journals in the area.

<span class="mw-page-title-main">Luca Cardelli</span> Italian computer scientist

Luca Andrea Cardelli is an Italian computer scientist who is a research professor at the University of Oxford, UK. Cardelli is well known for his research in type theory and operational semantics. Among other contributions, in programming languages, he helped design the language Modula-3, implemented the first compiler for the (non-pure) functional language ML, defined the concept of typeful programming, and helped develop the experimental language Polyphonic C#.

Robert Lyle Morris was an American psychologist, parapsychologist and professor at the University of Edinburgh, where he was the first holder of the Koestler Chair of Parapsychology at the Koestler Parapsychology Unit.

<span class="mw-page-title-main">Donald Michie</span> British artificial intelligence researcher

Donald Michie was a British researcher in artificial intelligence. During World War II, Michie worked for the Government Code and Cypher School at Bletchley Park, contributing to the effort to solve "Tunny", a German teleprinter cipher.

<span class="mw-page-title-main">Martin Hyland</span> British mathematician

(John) Martin Elliott Hyland is professor of mathematical logic at the University of Cambridge and a fellow of King's College, Cambridge. His interests include mathematical logic, category theory, and theoretical computer science.

<span class="mw-page-title-main">Alan Bundy</span> British artificial intelligence researcher (born 1947)

Alan Richard Bundy is a professor at the School of Informatics at the University of Edinburgh, known for his contributions to automated reasoning, especially to proof planning, the use of meta-level reasoning to guide proof search.

The ACM–IEEE Symposium on Logic in Computer Science (LICS) is an annual academic conference on the theory and practice of computer science in relation to mathematical logic. Extended versions of selected papers of each year's conference appear in renowned international journals such as Logical Methods in Computer Science and ACM Transactions on Computational Logic.

Li Wei is a Chinese computer scientist and a member of the Chinese Academy of Sciences. In 2002, he became President of Beihang University.

<span class="mw-page-title-main">Robert Stevens (scientist)</span>

Robert David Stevens is a professor of bio-health informatics. and former Head of Department of Computer Science at The University of Manchester

<span class="mw-page-title-main">Christopher Bishop</span> British computer scientist (born 1959)

Christopher Michael Bishop is a British computer scientist. He is a Microsoft Technical Fellow and Director of Microsoft Research AI4Science. He is also Honorary Professor of Computer Science at the University of Edinburgh, and a Fellow of Darwin College, Cambridge. Chris was a founding member of the UK AI Council, and in 2019 he was appointed to the Prime Minister’s Council for Science and Technology.

<span class="mw-page-title-main">Alan Robertson (geneticist)</span>

Alan Robertson was an English population geneticist. Originally a chemist, he was recruited after the Second World War to work on animal genetics on behalf of the British government, and continued in this sphere until his retirement in 1985. He was a major influence in the widespread adoption of artificial insemination of cattle.

Davide Sangiorgi is an Italian professor of computer science at the University of Bologna. He has previously held research positions at the University of Edinburgh and at Inria. He has received his PhD from the University of Edinburgh under the supervision of Robin Milner in 1993. He has had visiting positions at Centrum Wiskunde & Informatica, University of Cambridge, University of Oxford.

William Charles Earnshaw is Professor of Chromosome Dynamics at the University of Edinburgh, where he has been a Wellcome Trust Principal Research Fellow since 1996.

Alexandra Lascarides is a linguist and chair in Semantics in the School of Informatics at the University of Edinburgh. Her research investigates computational linguistics and artificial intelligence.

References

  1. 1 2 3 Anon (2013). "Plotkin, Prof. Gordon David" . Who's Who (online Oxford University Press  ed.). Oxford: A & C Black. doi:10.1093/ww/9780199540884.013.U31011.(Subscription or UK public library membership required.)
  2. 1 2 3 Gordon Plotkin at the Mathematics Genealogy Project
  3. 1 2 Plotkin, Gordon David (1972). Automatic methods of inductive inference (PhD thesis). University of Edinburgh. hdl:1842/6656. EThOS   uk.bl.ethos.482992. Lock-green.svg
  4. 1 2 Cardelli, Luca (1982). An algebraic approach to hardware description and verification (PhD thesis). University of Edinburgh. hdl:1842/13308. EThOS   uk.bl.ethos.253190.
  5. 1 2 Gardner, Philippa (1992). Representing logics in type theory (PhD thesis). University of Edinburgh. hdl:1842/14888. EThOS   uk.bl.ethos.651333. Lock-green.svg
  6. 1 2 Gurr, Douglas John (1990). Semantic frameworks for complexity (PhD thesis). University of Edinburgh. hdl:1842/13968. OCLC   475827463. EThOS   uk.bl.ethos.651894. Lock-green.svg
  7. 1 2 Moggi, Eugenio (1999). The partial lambda calculus (PhD thesis). University of Edinburgh. hdl:1842/419.
  8. 1 2 Wèi, Lǐ (1983). An operational approach to semantics and translation for programming languages (PhD thesis). hdl:1842/6636.
  9. Crary, Karl; Harper, Robert (2007). "Syntactic Logical Relations for Polymorphic and Recursive Types". Electronic Notes in Theoretical Computer Science. 172: 259. doi: 10.1016/j.entcs.2007.02.010 .
  10. Curien, Pierre-Louis (April 2022), Semantics and syntax, between computer science and mathematics (PDF), p. 2
  11. Gordon Plotkin publications indexed by Google Scholar OOjs UI icon edit-ltr-progressive.svg
  12. Gordon Plotkin author profile page at the ACM Digital Library
  13. Gordon Plotkin publications indexed by the Scopus bibliographic database. (subscription required)
  14. Gordon D. Plotkin at DBLP Bibliography Server OOjs UI icon edit-ltr-progressive.svg
  15. Mitchell, J. C.; Plotkin, G. D. (1988). "Abstract types have existential type". ACM Transactions on Programming Languages and Systems. 10 (3): 470. doi: 10.1145/44501.45065 . S2CID   1222153.
  16. Abadi, M. N.; Burrows, M.; Lampson, B.; Plotkin, G. (1993). "A calculus for access control in distributed systems" (PDF). ACM Transactions on Programming Languages and Systems. 15 (4): 706. CiteSeerX   10.1.1.72.3756 . doi:10.1145/155183.155225. hdl:1842/207. S2CID   13260508.
  17. "Symposium for Gordon Plotkin". www.lfcs.inf.ed.ac.uk.
  18. Plotkin, G. D. (1975). "Call-by-name, call-by-value and the λ-calculus". Theoretical Computer Science. 1 (2): 125–159. doi: 10.1016/0304-3975(75)90017-1 .
  19. Plotkin, G. D. (2004). "The origins of structural operational semantics". The Journal of Logic and Algebraic Programming. 60–61: 3–15. doi: 10.1016/j.jlap.2004.03.009 .
  20. A Structural Approach to Operational Semantics by G.D. Plotkin (1981)
  21. Program Verification and Semantics: Further Work Archived 26 September 2007 at the Wayback Machine (2004)
  22. Hoffmann, Ilire Hasani, Robert. "Academy of Europe: Plotkin Gordon". www.ae-info.org.{{cite web}}: CS1 maint: multiple names: authors list (link)
  23. "New Members of the American Academy of Arts and Sciences".
  24. "- Royal Society". royalsociety.org.
  25. "EC/1992/29: Plotkin, Gordon David". London: The Royal Society. Archived from the original on 16 April 2014.