レスリー・ランポート

レスリー・B・ランポート（Leslie B. Lamport、1941年2月7日 - ）は、アメリカ合衆国の計算機科学者である。
分散システムの先駆的な研究で知られる。文書作成システムLaTeXの最初の開発者であり、その最初のマニュアルの著者でもある。ランポートは、自律的に動作する複数のコンピュータがメッセージをやり取りして相互に通信を行う分散コンピューティングシステムの一見するとカオスな振る舞いに、明確でWell-definedな一貫性を課したことで、2013年のチューリング賞を受賞した。彼は、実際の分散システムの品質を向上させるための重要なアルゴリズムを考案し、その形式モデルと検証プロトコルを開発した。これらの貢献は、コンピュータシステムの正確性、性能、信頼性の向上につながっている。
若年期と教育.
ブロンクス科学高校を卒業した。マサチューセッツ工科大学で1960年に数学の学士号を、ブランダイス大学で1963年に数学の修士号、1972年に数学のPh.D.を取得した。彼の博士論文は解析的偏微分方程式の特異点に関するものであった。
キャリアと研究.
1970年から1977年まで(COMPASS)、1977年から1985年までSRIインターナショナル、1985年から2001年までデジタル・イクイップメント・コーポレーション（DEC、1998年にコンパックにより吸収合併）に計算機科学者として在籍した。2001年にカリフォルニア州マウンテンビューにあるマイクロソフトリサーチに入社した。
分散システム.
ランポートの研究は、分散システムの理論の基礎の構築に貢献してきた。彼の注目すべき論文には、以下のものがある。
これらの論文は、（および）やビザンチン障害などの概念に関連している。これらの論文は、計算機科学の分野で最も引用されている論文の一つであり、分散システムにおける多くの基本的な問題を解決するための、以下に掲げるアルゴリズムを記述している。
LaTeX.
1980年代初頭にドナルド・クヌースがTeXの初版をリリースしてから、ランポートは本を書きたいという個人的な欲求から、それが後に標準のマクロパッケージになることを期待して、TeXをベースにしたマクロのセットの作成を始めた。この一連のマクロは後にLaTeXとして知られるようになった。ランポートは1983年にの編集者であるピーター・ゴードンから、LaTeXのユーザーマニュアルを書籍化することを提案された。
1984年9月、ランポートはLaTeXのバージョン2.06aをリリースし、1985年8月にはランポートによるLaTeXの最後のバージョンであるLaTeX 2.09がリリースされた。1986年にランポートによる初のLaTeXユーザーマニュアル"LaTeX: A Document Preparation System"が刊行された。1989年8月21日、スタンフォード大学で開かれたTeXユーザーグループの会議で、ランポートはLaTeXのメンテナンスと開発をフランク・ミッテルバッハに移管することに同意した。ミッテルバッハはクリス・ローリー、Rainer SchöpfとともにLaTeX3チームを結成し、1994年にLaTeXの現在のバージョンであるLaTeX 2eをリリースした。
時相論理.
ランポートは時相論理の研究でも知られており、(TLA)を導入した。
最近の彼の貢献の中には、並行・反応型システムを指定・推論するための言語であるTLA+がある。彼は著書"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers"でこの言語について記述しており、この言語を「数学に対する技術者の反感を払拭するためのな試み」と定義している。
賞と栄誉.
2001年、ランポートの60歳の誕生日を記念して、第20回(PODC 2001)で一連の講演が企画された。