マイケル・J・C・ゴードン | |
|---|---|
 | |
| 生まれる | （1948年2月28日）1948年2月28日 |
| 死亡 | 2017年8月22日（2017年8月22日）（69歳） ケンブリッジ、イギリス |
| 母校 | ゴンヴィル・アンド・キーズ・カレッジ、ケンブリッジ大学 エディンバラ校 |
| 知られている | HOL定理証明器 |
| 科学者としてのキャリア | |
| フィールド | コンピュータサイエンス |
| 機関 | スタンフォード大学 ケンブリッジ大学 |
| 論文 | 純粋なLISPプログラムの評価と表示：意味論における実例 （1973） |
| 博士課程の指導教員 | ロッド・バーストール[1] |
マイケル・ジョン・コールドウェル・ゴードン FRS（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年からは、その範囲が高階論理におけるすべての定理証明にまで拡大されました。
参考文献
- ^ 数学系譜プロジェクトのマイケル・J・C・ゴードン
- ^ ab 「マイケル・J・C・ゴードンFRS、コンピュータ支援推論名誉教授、1948年2月28日 – 2017年8月22日」。訃報。英国：ケンブリッジ大学コンピュータ研究所。2017年。 2017年9月2日閲覧。
- ^ ケンブリッジ大学コンピュータ研究所（2017年10月27日）「マイケル・J・C・ゴードンFRS、コンピュータ支援推論教授（1948年2月28日 – 2017年8月22日）」『コンピューティングの形式的側面』29 (6)。Springer International Publishing , Inc. : 933. doi : 10.1007/s00165-017-0438-y。
- ^ ab Paulson, Lawrence C. (2018年6月11日). 「マイケル・ジョン・コールドウェル・ゴードン（FRS 1994）1948年2月28日 – 2017年8月22日」. arXiv : 1806.04002 . doi :10.1098/rsbm.2018.0019. S2CID 47017843.
{{cite journal}}:ジャーナルを引用するには|journal=（ヘルプ）が必要です - ^ ポールソン、ローレンス・C (2018). 「マイケル・ジョン・コールドウェル・ゴードン 1948年2月28日 – 2017年8月22日」王立協会フェロー伝記. doi.org/10.1098/rsbm.2018.0019.
- ^ 「システムインフラストラクチャの検証のためのツールとテクニック」 。 2023年1月14日閲覧。
- ^ Kalvala, Sara (2017年8月22日). 「マイク・ゴードンに関する悲しいニュース」HOL定理証明システム. SourceForge . 2017年9月2日閲覧。
- ^ Bowen, Jonathan P. (2020年6月). 「追悼：5人の形式手法の同僚へのトリビュート」(PDF) . FACS FACTS . 2020 (1). BCS-FACS : 13–29 . doi :10.13140/RG.2.2.13481.62560.
- ^ 「TPHOLS、高階論理における定理証明に関する会議」英国：ケンブリッジ大学。2008年5月7日時点のオリジナルよりアーカイブ。 2014年1月28日閲覧。
外部リンク
- マイク・ゴードンのホームページ
