John C. Reynolds - John C. Reynolds
John C. Reynolds | |
---|---|
Urodzony |
John Charles Reynolds
1 czerwca 1935 Stany Zjednoczone
|
Zmarły | 28 kwietnia 2013 | (w wieku 77)
Obywatelstwo | Stany Zjednoczone |
Edukacja |
Purdue University Ph.D. , Uniwersytet Harvarda (1961) |
Znany z | kontynuacje , interpretatory definicyjne , defunkcjonalizacja , Forsythe , język Gedanken , typy przecięć , polimorficzny rachunek lambda , parametryczność relacyjna , logika separacji , ALGOL |
Nagrody | Medal Lovelace (2010) |
Kariera naukowa | |
Pola | Informatyk |
Instytucje |
Uniwersytet w Syracuse Uniwersytet Carnegie Mellon |
Praca dyplomowa | Właściwości powierzchni materii jądrowej (1961) |
Doktoranci | Benjamin C. Pierce |
Stronie internetowej | www |
John Charles Reynolds (1 czerwca 1935 – 28 kwietnia 2013) był amerykańskim informatykiem .
Edukacja i afiliacje
John Reynolds studiował na Purdue University , a następnie zarobił Doktor filozofii (Ph.D.) w fizyce teoretycznej z Uniwersytetu Harvarda w 1961 roku był profesorem informatyki na Uniwersytecie Syracuse od 1970 do 1986. Od tego czasu aż do śmierci był profesor informatyki na Uniwersytecie Carnegie Mellon . Zajmował również stanowiska wizytujące na Uniwersytecie Aarhus ( Dania ), Uniwersytecie Edynburskim , Imperial College London , Microsoft Research ( Cambridge ) oraz Queen Mary na Uniwersytecie Londyńskim w Wielkiej Brytanii (Wielka Brytania).
Praca akademicka
Główne zainteresowania badawcze Reynoldsa dotyczyły projektowania języków programowania i związanych z nimi języków specyfikacji , szczególnie w zakresie semantyki formalnej . Wynalazł polimorficzny rachunek lambda (System F) i sformułował własność parametryczności semantycznej ; ten sam rachunek został niezależnie odkryty przez Jean-Yves Girarda . Napisał przełomowy artykuł o interpretatorach definicji, wyjaśniający wczesne prace nad kontynuacją i wprowadzający technikę defunkcjonalizacji . Zastosował teorię kategorii do semantyki języka programowania . Zdefiniował języki programowania Gedanken i Forsythe, znane z używania typów skrzyżowań . Pracował nad logiką separacji w celu opisania i uzasadnienia wspólnych mutowalnych struktur danych .
Reynolds stworzył eleganckie, wyidealizowane sformułowanie języka programowania ALGOL , który wykazuje czystość składniową i semantyczną ALGOL i jest używany w badaniach nad językiem programowania. Przedstawił również przekonujący argument metodologiczny dotyczący przydatności efektów lokalnych w kontekście języków call-by-name , w przeciwieństwie do efektów globalnych używanych przez języki call-by-value , takie jak ML . Konceptualna spójność języka uczyniła go jednym z głównych obiektów badań semantycznych, obok Programowania Funkcji Obliczeniowych (PCF) i ML.
Był redaktorem czasopism takich jak Communications of the ACM i Journal of the ACM . W 2001 roku został mianowany Fellow of the Association for Computing Machinery (ACM). Zdobył nagrodę ACM SIGPLAN Programming Language Achievement Award w 2003 roku oraz Lovelace Medal od British Computer Society w 2010 roku.
Wybrane publikacje
- Książki
- Rzemiosło programowania , Prentice Hall International, 1981. ISBN 0-13-188862-5 .
- Teorie języków programowania , Cambridge University Press , 1998. ISBN 0-521-59414-6 .
- Artykuły
- „Systemy transformacyjne i struktura algebraiczna formuł atomowych” (PDF) . Inteligencja maszynowa . 5 : 135–151. 1970.
- „W stronę teorii budowy typów” . Colloque sur la Programmation . Paryż, Francja. 1974. s. 408-425. doi : 10.1007/3-540-06859-7_148 .
- „Typy, abstrakcja i polimorfizm parametryczny” (PDF) . Przetwarzanie informacji '83 . 1983. s. 513-523.
- „Logika separacji: logika dla wspólnych mutowalnych struktur danych” (PDF) . XVII Sympozjum IEEE na temat logiki w informatyce (LICS 2002) . s. 55-74. doi : 10.1109/LICS.2002.1029817 .
Bibliografia
Dalsza lektura
- Olivier Danvy , Peter O'Hearn i Philip Wadler (redaktorzy), „ Festschrift na 70. urodziny Johna C. Reynoldsa ”. Informatyka teoretyczna , 375(1–3):1–350, 1 maja 2007. Od redakcji, strony 1–2. doi : 10.1016/j.tcs.2006.12.024
- Stephen Brookes , Peter O'Hearn i Uday Reddy , „ Esencja Reynoldsa ”. POPL 2014, s. 251–256. Doi : 10.1145/2535838.2537851
Linki zewnętrzne
- Oficjalna strona internetowa
- Życiorys
- John C. Reynolds w DBLP Bibliography Server
- John C. Reynolds w projekcie Genealogia Matematyki
- Weryfikacja programu i semantyka: dalsza praca (Londyn, 2004)