マイケル・J・C・ゴードン

マイケル・J・C・ゴードン
生まれる	( 1948-02-28 )1948年2月28日 リポン、ヨークシャー、イングランド
死亡	2017年8月22日(2017-08-22)（69歳） ケンブリッジ、イギリス
母校	ゴンヴィル・アンド・キース・カレッジ、ケンブリッジ大学 エディンバラ校
知られている	HOL定理証明器
科学者としてのキャリア
フィールド	コンピュータサイエンス
機関	スタンフォード大学 ケンブリッジ大学
論文	純粋な LISP プログラムの評価と表記: 意味論における実例 (1973)
博士課程の指導教員	ロッド・バーストール[1]

マイケル・ジョン・コールドウェル ・ゴードン（1948年2月28日 - 2017年8月22日）はイギリスのコンピュータ科学者であった。^{[2] [3]}

マイク・ゴードンはイギリスのヨークシャー州リポンで生まれました。^[4]ダーティントン・ホール・スクールとベデールズ・スクールに通いました。1966年、ケンブリッジ大学ゴンヴィル・アンド・キーズ・カレッジで工学を学ぶために受け入れられましたが、数学に転向しました。在学中の1969年、夏にロンドンの国立物理学研究所で働き、初めてコンピューターに触れました。

ゴードンは、エディンバラ大学でロッド・バーストールの指導の下で博士号を取得し、1973年に「純粋なLISPプログラムの評価と表示」と題する論文で博士号を取得しました。彼は、 LISPの発明者であるジョン・マッカーシーに招かれ、カリフォルニア州スタンフォード大学にある彼の人工知能研究所で働きました。ゴードンは、1981年からケンブリッジ大学コンピュータ研究所で講師として働き、 1988年にリーダーに昇進し、 1996年に教授になりました。

彼は1994年に王立協会の会員に選出され、 ^{[5] 2008年には彼の60歳の誕生日を記念して、}システムインフラストラクチャの検証のためのツールとテクニックに関する2日間の研究会がそこで開催されました。^[6]

マイク・ゴードンは、エディンバラ大学のロビン・ミルナーの博士課程の学生であったアヴラ・コーンと結婚し、一緒に研究を行っていた。^[4]

彼は短い闘病の後にケンブリッジで亡くなり、妻と二人の息子が残された。^{[2] [7] [8]}

ゴードンはHOL 定理証明器の開発を主導しました。HOL システムは、高階論理における対話型の定理証明環境です。その最も優れた特徴は、メタ言語MLによる高度なプログラミング可能性です。このシステムは、純粋数学の形式化から産業用ハードウェアの検証まで、さまざまな用途に使用されています。

HOLシステムに関する一連の国際会議、TPHOLが開催されてきました。^[9]最初の3回は非公式のユーザー会議で、議事録は出版されませんでした。現在は、前回の会議の開催地とは別の大陸で毎年会議を開催するのが伝統となっています。1996年からは、その範囲が拡大し、高階論理におけるすべての定理証明を網羅するようになりました。

• マイク・ゴードンのホームページ