Loading article…
グレッグ・ネルソン | |
|---|---|
| 生まれる | チャールズ・グレゴリー・ネルソン 1953年3月27日 |
| 死亡 | 2015年2月2日（61歳） |
| 教育 | ハーバード大学学士（1976年）スタンフォード大学 博士（1980年） |
| 知られている | 理論を法とした充足可能性 拡張された静的検査 プログラム検証 Modula-3委員会 ESC/Java定理証明器の簡素化 |
| 受賞歴 | エルブラン賞（2013） |
| 科学者としてのキャリア | |
| 機関 | ゼロックス パロアルト研究所(PARC) デジタル イクイップメント コーポレーション(DEC)システム リサーチ センター(SRC) ヒューレット パッカード研究所 |
| 論文 | プログラム検証のテクニック (1980) |
| 博士課程の指導教員 | ロバート・タージャン |
チャールズ・グレゴリー・ネルソン（1953年3月27日 - 2015年2月2日）はアメリカのコンピュータ科学者である。[1] [2]
バイオグラフィー
ネルソンはホノルルで育ちました。少年時代は体操とテニスが得意でした。大学の実験学校に通いました。 1976年にハーバード大学で数学の学士号を取得しました。1980年にロバート・タージャンの指導の下、スタンフォード大学でコンピューターサイエンスの博士号を取得しました。サンフランシスコ湾岸地域に永住する前には、アラスカ州ジュノーに1年間住んでいました。
注目すべき作品
彼の論文「プログラム検証の技法」[3]は、プログラム検証と自動定理証明の両方に影響を与え、特に現在では理論を法とした充足可能性と呼ばれる分野で、決定手順を組み合わせる技法や、一階述語論理と項代数における量指定子のない制約に対する効率的な決定手順に貢献しました。彼は2013年にエルブラン賞を受賞しました。 [4]
定理証明とプログラム検証への先駆的な貢献、例えば、デレク・オッペンとの充足可能性手順と高速合同閉包アルゴリズムの組み合わせに関する独創的な研究、非常に影響力のある定理証明器 Simplify の開発、拡張静的検査分野の創設における役割などに対して。
彼は、 ESC/Javaで使用されるSimplify定理証明器の開発に尽力しました。彼は他のいくつかの分野でも重要な貢献をしました。彼はModula-3委員会のメンバーとしてプログラミング言語設計の分野に貢献しました。分散システムでは、Network Objects に貢献しました。彼は、制約ベースのグラフィック エディター (Juno および Juno-2)、ウィンドウ システム(Trestle)、最適コード生成(Denali)、およびマルチスレッドプログラミング (Eraser) で先駆的な貢献をしました。
参照
参考文献
- ^ Perl, Sharon (2015年2月). 「Greg Nelson: 1953年3月27日 – 2015年2月2日」. Palo Alto Online .カリフォルニア州パロアルト. 2021年4月15日閲覧。
- ^ Perl, Sharon (2015年3月4日). 「Greg Nelson」. Honolulu Star-Advertiser: Obituaries .ホノルル、ハワイ. 2021年4月15日閲覧。
- ^ ネルソン、グレッグ (1980–1981)。プログラム検証のテクニック(PDF)。電気工学およびコンピュータサイエンス学部(PhD)。カリフォルニア大学バークレー校。 2021年4月13日閲覧。
- ^ Montmirail, Valentin; Sutcliffe, Geoff (2013 年 6 月)。「Herbrand Award: for Distinguished Contributions to Automated Reasoning」。自動推論に関する会議。2021年 4 月 13 日閲覧。