Лесли Лампорт - Leslie Lamport

Лесли Лампорт
Leslie Lamport.jpg
Туған
Лесли Б. Лампорт

(1941-02-07) 1941 ж. 7 ақпан (79 жас)
Нью-Йорк қаласы, Нью Йорк
Алма матер
Белгілі
Марапаттар
Ғылыми мансап
ӨрістерИнформатика
Мекемелер
ДиссертацияСингулярлы мәліметтермен аналитикалық Коши есебі  (1972)
Докторантура кеңесшісіРичард Палеис[1]
Веб-сайтлампорт.org

Лесли Б. Лампорт (1941 жылы 7 ақпанда дүниеге келген) - бұл Американдық информатик. Лампорт өзінің негізгі жұмысымен танымал бөлінген жүйелер, және құжаттарды дайындау жүйесінің алғашқы әзірлеушісі ретінде LaTeX және оның алғашқы нұсқаулығының авторы.[2][3] Лесли Лампорт 2013 жылдың жеңімпазы болды Тюринг сыйлығы[4] хаосты болып көрінетін мінез-құлыққа нақты, анықталған келісімділік енгізу үшін таратылған есептеу бірнеше автономды компьютерлер бір-бірімен хабарлама жіберу арқылы байланысатын жүйелер. Ол маңызды нәрсе ойлап тапты алгоритмдер және дамыған формальды модельдеу және нақты таратылған жүйелердің сапасын жақсартатын тексеру хаттамалары. Бұл үлестер компьютерлік жүйелердің дұрыстығын, өнімділігі мен сенімділігін арттырды.[5][6][7][8][9]

Ерте өмірі және білімі

Түлегі Бронкс жоғары ғылыми мектебі, ол алды B.S. жылы математика бастап Массачусетс технологиялық институты 1960 жылы және М.А. және Ph.D. математика дәрежесі Брандеис университеті сәйкесінше 1963 және 1972 жылдары.[10] Оның диссертациясы аналитикалық ерекшеліктер туралы болды дербес дифференциалдық теңдеулер.[11]

Мансап және зерттеу

Лампорт информатик болып жұмыс істеді Massachusetts Computer Associates 1970 жылдан 1977 жылға дейін, Халықаралық ҒЗИ 1977 жылдан 1985 жылға дейін және Digital Equipment Corporation және Compaq 1985 жылдан 2001 жылға дейін. 2001 жылы ол қосылды Microsoft Research жылы Маунтин-Вью, Калифорния, ол 2014 жылы жабылды.[10]

Таратылған жүйелер

Лампорттың зерттеулері үлестірілген жүйелер теориясының негізін қалады. Оның ең танымал қағаздарының арасында

Бұл құжаттар сияқты ұғымдарға қатысты логикалық сағаттар (және бұрын болған қатынас) және Византиядағы сәтсіздіктер. Олар информатика саласындағы ең көп дәйексөз болып табылады,[17] таралған жүйелердегі көптеген іргелі мәселелерді шешудің алгоритмдерін сипаттаңыз, соның ішінде:

LaTeX

Қашан Дональд Кнут ерте шығарылымдарын шығара бастады TeX 1980 жылдардың басында Лампорт - кітап жазудың жеке қажеттілігіне байланысты - кейінірек оның стандартты макробумасы болады деп үміттеніп, оған негізделген макростар жиынтығында жұмыс істей бастады. Бұл макростар жиынтығы кейінірек белгілі болады LaTeX, ол үшін кейіннен Лампортқа 1983 жылы Питер Гордон, ан Аддисон-Уэсли Lamport пайдаланушы нұсқаулығын кітапқа айналдыруды ұсынған редактор.[18][19]

1984 жылдың қыркүйегінде Lamport LaTeX макростарының 2.06a нұсқасын шығарды, ал 1985 жылдың тамызында LaTeX 2.09 - Lamport-тың LaTeX соңғы нұсқасы да шығарылады. Сонымен бірге, Addison-Wesley Lamport компаниясының алғашқы LaTeX пайдаланушы нұсқаулығын шығарды, LaTeX: Құжаттарды дайындау жүйесі, 1986 жылы «бірнеше жүз мыңнан астам» дананы сатты деп болжанған және 1989 жылы 21 тамызда TeX пайдаланушылар тобының отырысында Стэнфорд, Лампорт LaTeX-ті күтіп-ұстау мен дамытуды Фрэнк Миттелбахқа тапсыруға келіседі, ол Крис Роули және Райнер Шёпфпен бірге LaTeX3 командасын құрып, кейін LaTeX-тің 1994 жылғы қолданыстағы нұсқасы LaTeX 2e шығарады.[19][3][20]

Уақытша логика

Лампорт сонымен бірге өзінің жұмысымен танымал уақытша логика, онда ол іс-әрекеттің уақытша логикасы (TLA).[21][22] Оның соңғы салымдарының арасында TLA+, кітабында сипаттайтын параллельді және реактивті жүйелер туралы анықтама беру және пікір айту тілі Жүйелерді көрсету: TLA+ Аппараттық және бағдарламалық жасақтама инженерлеріне арналған тіл және құралдар[23] және «ретінде анықтайдыкикотикалық математикаға деген инженерлердің антипатиясын жеңуге тырысу ».[24]

Марапаттар мен марапаттар

Lamport 2013 алды Тюринг сыйлығы 2014 жылы «үлестірілген және қатарлас жүйелер теориясы мен практикасына іргелі үлестер, атап айтқанда себептілік және логикалық сағаттар, қауіпсіздік пен тіршілік, қайталанатын күй машиналары және дәйектілік сияқты ұғымдарды ойлап табу» үшін.[25] Ол стипендиат болып сайланды ACM 2014 жылы үлестірілген және қатарлас жүйелер теориясы мен практикасына қосқан үлесі үшін.[26] Ол сондай-ақ еуропалық университеттердің бес құрметті докторларын алды: Ренн университеті және Христиан Альбрехтс атындағы Киль университеті 2003 жылы, EPFL 2004 жылы, Лугано университеті 2006 жылы және Нэнси-Университет 2007 жылы.[10] 2004 жылы ол алды IEEE Emanuel R. Piore сыйлығы.[27] 2005 ж. «Ақаулар болған кезде келісімге қол қою»[28] алды Дайкстра сыйлығы.[29] Лампорттың алпыс жасқа толуына орай, 20-да дәрістер сериясы ұйымдастырылды Таратылған есептеу принциптері туралы симпозиум (PODC 2001).[30] 2008 жылы ол алды IEEE Джон фон Нейман медалі.[31] 2011 жылы ол сайланды Америка Құрама Штаттарының Ұлттық ғылым академиясы.[32]

Әдебиеттер тізімі

  1. ^ Лесли Лампорт кезінде Математика шежіресі жобасы Мұны Wikidata-да өңдеңіз
  2. ^ Лампорт, Лесли (1986). LaTeX: Құжаттарды дайындау жүйесі. Аддисон-Уэсли. ISBN  978-0-201-15790-1. Алынған 2019-06-20.
  3. ^ а б «LaTeX, кәсіби теру және ғылыми баспаға арналған нақты, техникалық емес кіріспе». Математикалық қойма. 2015-09-05. Алынған 2019-07-19.
  4. ^ Лампорт, Лесли (2013). «Лесли Лампорт - А.М. Тьюринг сыйлығының иегері». ACM.
  5. ^ Лесли Лампорт авторлық профиль парағы ACM Сандық кітапхана
  6. ^ а б Лампорт, Л. (1978). «Таратылған жүйеде уақыт, сағаттар және іс-шаралардың реті» (PDF). ACM байланысы . 21 (7): 558–565. CiteSeerX  10.1.1.142.3682. дои:10.1145/359545.359563. S2CID  215822405.
  7. ^ Жарияланымдар тізімі бастап Microsoft Academic
  8. ^ Savage, N. (2014). «Жалпы келісім: Лесли Лампорт мақсатты түрде жұмыс істейтін үлестірілген есептеу жүйелерін құру теориясы мен практикасына үлес қосты». ACM байланысы. 57 (6): 22–23. дои:10.1145/2601076. S2CID  5936915.
  9. ^ Хофманн, Л. (2014). «Сұрақтар мен жауаптарды бөлу және жеңу: Лизли Лампорт Византия генералдары, сағаттары және бір уақытта жұмыс істейтін жүйелер туралы ой қозғау құралдары туралы». ACM байланысы. 57 (6): 112-фф. дои:10.1145/2601077. S2CID  31514650.
  10. ^ а б c Лампорт, Лесли (2006-12-19). «Менің жазбаларым». Алынған 2007-02-02.
  11. ^ Лампорт, Лесли (1972). «Сингулярлық мәліметтерге қатысты аналитикалық Коши проблемасы». Алынған 2007-02-02. Журналға сілтеме жасау қажет | журнал = (Көмектесіңдер)
  12. ^ Neiger, Gil (2003-01-23). «PODC ықпалды қағаз сыйлығы: 2000». Архивтелген түпнұсқа 2013-07-09. Алынған 2007-02-02.
  13. ^ Лампорт, Лесли (1979). «Мультипроцессорлық бағдарламаны дұрыс орындайтын мультипроцессорлық компьютерді қалай жасауға болады». IEEE Транс. Есептеу. 28 (9): 690–691. дои:10.1109 / TC.1979.1675439. ISSN  0018-9340. S2CID  5679366.
  14. ^ Лампорт, Лесли; Роберт Шостак; Маршалл Пийз (шілде 1982). «Византия генералдары проблемасы». Бағдарламалау тілдері мен жүйелері бойынша ACM транзакциялары. 4 (3): 382–401. CiteSeerX  10.1.1.64.2312. дои:10.1145/357172.357176. Алынған 2007-02-02.
  15. ^ Чанди, К.Мани; Лесли Лампорт (ақпан 1985). «Таратылған суреттер: Таратылған жүйенің ғаламдық күйін анықтау». Компьютерлік жүйелердегі ACM транзакциялары. 3 (1): 63–75. CiteSeerX  10.1.1.69.2561. дои:10.1145/214451.214456. S2CID  207193167. Алынған 2007-02-02.
  16. ^ Лампорт, Лесли (мамыр 1998). «Толық емес парламент». Компьютерлік жүйелердегі ACM транзакциялары. 16 (2): 133–169. дои:10.1145/279227.279229. S2CID  421028. Алынған 2007-02-02.
  17. ^ «Информатикадағы ең көп сілтеме жасалған мақалалар». Қыркүйек 2006. Алынған 2007-10-08.
  18. ^ Лампорт, Лесли. «Математиканың бет-бейнесін қалай өзгертті (LA)» (PDF).
  19. ^ а б «Лесли Лампорттың жазбалары». lamport.azurewebsites.net. Алынған 2019-07-19.
  20. ^ «TeX, LaTeX және AMS-LaTeX». 1998-12-03. Мұрағатталды түпнұсқадан 1998-12-03 жж. Алынған 2019-07-19.
  21. ^ Лампорт, Лесли (1990-04-01). «Іс-әрекеттің уақытша логикасы». Алынған 2007-02-02. Журналға сілтеме жасау қажет | журнал = (Көмектесіңдер)
  22. ^ Лампорт, Лесли (мамыр 1994). «Іс-әрекеттің уақытша логикасы». Бағдарламалау тілдері мен жүйелері бойынша ACM транзакциялары. 16 (3): 872–923. дои:10.1145/177492.177726. S2CID  5498471. Алынған 2007-02-02.
  23. ^ Лампорт, Лесли (2002). Жүйелерді көрсету: TLA+ Аппараттық және бағдарламалық жасақтама инженерлеріне арналған тіл және құралдар. Аддисон-Уэсли. ISBN  978-0-321-14306-8. Алынған 2007-02-02.
  24. ^ «Халықаралық конференциялардың сенімді жүйелері мен желілері бойынша конференциясы негізгі баяндамашының өмірбаяны». Алынған 2007-03-06.
  25. ^ «2013 жылғы Тьюринг сыйлығы». ACM.
  26. ^ Лесли Лампорт ACM стипендиаттары 2014 ж
  27. ^ «IEEE Emanuel R. Piore сыйлығының иегерлері es» (PDF). IEEE. Архивтелген түпнұсқа (PDF) 2010-11-24. Алынған 2010-12-31.
  28. ^ Пиз, Маршалл; Роберт Шостак; Лесли Лампорт (1980 ж. Сәуір). «Ақаулар болған кезде келісімге келу». Есептеу техникасы қауымдастығының журналы. 27 (2): 228–234. CiteSeerX  10.1.1.68.4044. дои:10.1145/322186.322188. S2CID  6429068. Алынған 2007-02-02.
  29. ^ «Таратылған есептеуіш техникасы бойынша Эдсгер В. Дайкстра сыйлығы: 2005». Алынған 2007-02-02.
  30. ^ «PODC 2001: Lamport дәрістер сериясы». Алынған 2009-07-02.
  31. ^ «IEEE Джон фон Нейман медалін алушылар» (PDF). IEEE. Алынған 31 желтоқсан, 2010.
  32. ^ Сайланған мүшелер мен шетелдік қауымдастықтар Мұрағатталды 2011 жылғы 7 мамырда Wayback Machine, Ұлттық ғылым академиясы, 3 мамыр 2011 ж.

Сыртқы сілтемелер