ローレンス・ポールソン

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

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

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

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

ポールソンは2017年に王立協会フェロー（FRS）に選出され^{[ 2 ]}、2008年には計算機学会フェロー[ ^{4 ] 、}ミュンヘン工科大学の情報学における論理学の特別客員教授に選出された^{[ 21 ]}。

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