Leslie Lamport

Leslie Lamport
Leslie Lamport.jpg
Född ( 1941-02-07 ) 7 februari 1941 (82 år)
Nationalitet amerikansk
Alma mater
Känd för
Utmärkelser
Vetenskaplig karriär
Fält Datavetenskap
institutioner
Avhandling   Det analytiska Cauchy-problemet med singular data (1972)
Doktorandrådgivare Richard Palais
Hemsida lamport .org

Leslie B. Lamport (född 7 februari 1941 i Brooklyn ) är en amerikansk datavetare och matematiker . Lamport är mest känd för sitt framstående arbete inom distribuerade system , och som den första utvecklaren av dokumentförberedelsesystemet LaTeX och författaren till dess första manual.

Lamport vann 2013 års Turing Award för att ha påtvingat tydlig, väldefinierad koherens i det till synes kaotiska beteendet hos distribuerade datorsystem, där flera autonoma datorer kommunicerar med varandra genom att skicka meddelanden. Han tog fram viktiga algoritmer och utvecklade formella modellerings- och verifieringsprotokoll som förbättrar kvaliteten på verkliga distribuerade system. Dessa bidrag har resulterat i förbättrad korrekthet, prestanda och tillförlitlighet hos datorsystem.

tidigt liv och utbildning

Lamport föddes i en judisk familj i Brooklyn, New York, son till Benjamin och Hannah Lamport (född Lasser). Hans far var en invandrare från Volkovisk i det ryska imperiet (nuvarande Vawkavysk , Vitryssland ) och hans mor var en immigrant från det österrikisk-ungerska riket, nu sydöstra Polen.

tog examen från Bronx High School of Science och fick en BS i matematik från Massachusetts Institute of Technology 1960, följt av MA (1963) och Ph.D. (1972) grader i matematik från Brandeis University . Hans avhandling, The analytic Cauchy problem with singular data , handlar om singulariteter i analytiska partiella differentialekvationer .

Karriär och forskning

Lamport arbetade som datavetare vid Massachusetts Computer Associates från 1970 till 1977, SRI International från 1977 till 1985, och Digital Equipment Corporation och Compaq från 1985 till 2001. 2001 började han med Microsoft Research i Kalifornien .

Distribuerade system

Lamports forskningsbidrag har lagt grunden till teorin om distribuerade system. Bland hans mest anmärkningsvärda papper är

Dessa papper relaterar till sådana begrepp som logiska klockor (och hände-före- relationen) och bysantinska misslyckanden . De är bland de mest citerade artiklarna inom datavetenskap och beskriver algoritmer för att lösa många grundläggande problem i distribuerade system, inklusive:

Latex

När Donald Knuth började ge ut de tidiga utgåvorna av TeX i början av 1980-talet började Lamport – på grund av sitt personliga behov av att skriva en bok – också arbeta på en uppsättning makron baserade på den, i hopp om att den senare skulle bli dess standard makropaket. Denna uppsättning makron skulle senare bli känd som LaTeX , för vilken Lamport senare skulle kontaktas 1983 av Peter Gordon, en Addison-Wesley- redaktör, som föreslog att Lamport skulle förvandla sin användarmanual till en bok.

I september 1984 släppte Lamport version 2.06a av LaTeX-makron, och i augusti 1985 skulle LaTeX 2.09 – den sista versionen av Lamports LaTeX – också släppas. Samtidigt släppte Addison-Wesley Lamports första LaTeX-användarmanual, LaTeX: A Document Preparation System , 1986, som påstås sålde "mer än några hundra tusen" exemplar, och den 21 augusti 1989 vid ett TeX User Group-möte i Stanford , skulle Lamport gå med på att överlåta underhållet och utvecklingen av LaTeX till Frank Mittelbach, som tillsammans med Chris Rowley och Rainer Schöpf skulle bilda LaTeX3-teamet, och sedan släppa LaTeX 2e, den nuvarande versionen av LaTeX, 1994.

Temporal logik

Lamport är också känd för sitt arbete med tidslogik , där han introducerade handlingens tidslogik (TLA). Bland hans nyare bidrag finns TLA + , ett språk för att specificera och resonera kring samtidiga och reaktiva system, som han beskriver i boken Specificing Systems: The TLA + Language and Tools for Hardware and Software Engineers. Han definierar TLA+ som ett " quixotiskt försök att övervinna ingenjörers antipati mot matematik".

Pris och ära

Lamport fick 2013 års Turing Award för "grundläggande bidrag till teorin och praktiken av distribuerade och samtidiga system, särskilt uppfinningen av begrepp som kausalitet och logiska klockor, säkerhet och livlighet, replikerade tillståndsmaskiner och sekventiell konsistens" 2014. Han var valdes till medlem av National Academy of Engineering 1991 för bidrag till de teoretiska grunderna för samtidig och feltolerant datoranvändning. Han valdes till Fellow of Association for Computing Machinery för grundläggande bidrag till teorin och praktiken av distribuerade och samtidiga system 2014. Han fick också fem hedersdoktorer från europeiska universitet: University of Rennes och Christian Albrechts University of Kiel 2003, École Polytechnique Fédérale de Lausanne (EPFL) 2004, University of Lugano 2006 och Nancy-Université 2007. 2004 mottog han IEEE Emanuel R. Piore Award . År 2005 mottog tidningen "Att nå överenskommelsen i närvaro av fel" Dijkstra-priset . För att hedra Lamports sextioårsdag anordnades en föreläsningsserie vid det 20:e symposiet om principer för distribuerad datoranvändning ( PODC 2001). 2008 mottog han IEEE John von Neumann-medaljen . 2011 valdes han in i National Academy of Sciences .

externa länkar