ローレンス・ポールソン

ローレンス・ポールソン フランス
2017年のポールソン
生まれる	ローレンス・チャールズ・ポールソン 1955年（68歳～69歳）[4]
市民権	米国/英国
母校	カリフォルニア工科大学 スタンフォード大学
知られている	ML イザベル[5] メティタルスキ[6]
配偶者たち	スーザン・メアリー・ポールソン（2010年没） エレナ・チュグノヴァ
受賞歴	ACMフェロー（2008）[1]
科学者としてのキャリア
フィールド	定理証明[2] 形式手法[2] コンピュータセキュリティ[2]
機関	ケンブリッジ大学 ミュンヘン工科大学
論文	意味文法のコンパイラジェネレータ (1981)
博士課程の指導教員	ジョン・L・ヘネシー[3]
Webサイト	英文

ローレンス・チャールズ・ポールソンはアメリカのコンピュータ科学者である。ケンブリッジ大学コンピュータ研究所の計算論理学教授であり、ケンブリッジ大学クレア・カレッジの研究員でもある。^{[2] [3] [7] [8] [9]}

ポールソンは1977年にカリフォルニア工科大学を卒業し、 ^{[10] 1981年に}ジョン・L・ヘネシーの指導の下、プログラミング言語とコンパイラに関する研究でスタンフォード大学でコンピュータサイエンスの博士号を取得しました。^{[3] [11]}

ポールソンは1983年にケンブリッジ大学に着任し、1987年にケンブリッジ大学クレア・カレッジのフェローとなった。彼はプログラミング言語MLの基礎となる著書『ML for the Working Programmer 』で最もよく知られている。^{[12] [13]}彼の研究は1986年に発表した対話型定理証明器Isabelleを中心に展開している。 ^[14]彼は帰納的定義を用いた暗号プロトコルの検証に取り組んでおり、^[15]また、クルト・ゲーデルの構成可能宇宙を形式化した。最近、彼は実数値の特殊関数用の新しい定理証明器 MetiTarski ^{[6]を構築した。 [16]}

ポールソンは、コンピュータサイエンストリポスで「論理と証明^」[17]と題した学部講義を教えており、自動定理証明と関連手法を扱っています。（彼はかつて関数型プログラミングを紹介する「コンピュータサイエンスの基礎」^{[18]を教えていましたが、このコースは2017年に}アラン・マイクロフトとアマンダ・プロロックに引き継がれ、 ^[19]、 2019年にはアニル・マダヴァペディとアマンダ・プロロックに引き継がれました^[20]）。

ポールソンは2017年に王立協会（FRS）のフェローに選出され、^[5] 2008年には計算機協会のフェローに選出され^{[1] 、}ミュンヘン工科大学の情報科学論理学の著名な准教授にも就任した。^{[いつ? ] [21]}

ポールソンには、2010年に亡くなった最初の妻スーザン・メアリー・ポールソン博士との間に2人の子供がいる。^[22] 2012年からはエレナ・チュグノワ博士と結婚している。^[4]