トビアス・ニプコウ

トビアス・ニプコウ
生誕	1958年（67～68歳）
著名な	Isabelle 証明アシスタント
科学的なキャリア
所属機関	マサチューセッツ工科大学（MIT）、ケンブリッジ大学、ミュンヘン工科大学
論文	非決定性データ型の振る舞い実装概念 （1987）
博士課程指導教員	クリフ・B・ジョーンズ
ウェブサイト	www21.in.tum.de /~nipkow

トビアス・ニプコウ（1958年生まれ）はドイツのコンピューター科学者です。

経歴

ニプコウは1982年にダルムシュタット工科大学コンピュータサイエンス科でコンピュータサイエンスの修士号（ディプロム）を取得し、1987年に マンチェスター大学で博士号を取得しました

1987年からMITに勤務し、1989年にケンブリッジ大学、 1992年にミュンヘン工科大学に移り、プログラミング理論の教授に任命された。

彼は 2011 年からロジックおよび検証グループの議長を務めています。

彼は対話型および自動定理証明、特にIsabelle証明支援ツールの研究で知られており、 2021年1月1日までJournal of Automated Reasoningの編集者を務めていた。^{[ 1 ]}さらに、プログラミング言語の意味論、型システム、関数型プログラミングにも力を入れている。^{[ 2 ]}

2021年に彼は「Isabelleと関連ツールの開発におけるリーダーシップ、幅広いアプリケーションにおける証明支援システムの基礎、自動化、および使用への重要な貢献、ならびに自動推論の可視性を高めるための成功した取り組みが認められて」エルブラン賞を受賞した。 ^{[ 3 ]}

2022年にアカデミア・ヨーロッパの会員に選出された。^{[ 4 ]}

選定された出版物

• Martin, U. & Nipkow, T. (1986). 「ブール環における統一」. Jörg H. Siekmann (編). Proc. 8th Conference on Automated Deduction . LNCS . Vol. 230. Springer. pp.  506– 513
• Tobias Nipkow (1987).非決定性データ型の振る舞い実装コンセプト(博士論文). コンピュータサイエンス学科報告書. Vol. UMCS-87-5-3. マンチェスター大学.
• Nipkow, T. (1989). 「マッチングアルゴリズムの組み合わせ：長方形の場合」. Nachum Dershowitz (編).書き換え技術とその応用, 第3回国際会議, RTA-89 . LNCS. 第355巻. Springer. pp.  343– 358.
• トビアス・ニプコウ (1990). 「原始代数における統一、その冪とその多様体」 . ACMジャーナル. 37 (4): 742– 776. doi : 10.1145/96559.96569 . S2CID  14940917 .
• Nipkow, T. & Qian, Z. (1991). 「モジュラー高階電子統合」. Ronald V. (編). 書誌情報.書き換え技術とその応用, 第4回国際会議, RTA-91 . LNCS. 第488巻. Springer. pp.  200– 214.
• トビアス・ニプコウ (1991). 「高階臨界対」.第6回IEEEコンピュータサイエンス論理シンポジウム論文集. pp.  342– 349.
• Nipkow, T. (1995). 「高階書き換えシステム（招待講演）」. Hsiang, Jieh (編).第6回書き換え技術と応用に関する国際会議 (RTA) . LNCS. 第914巻. Springer. p. 256.
• フランツ・バーダー、トビアス・ニプコウ（1998年）『用語の書き換えとそのすべて』ケンブリッジ：ケンブリッジ大学出版局。ISBN 978-0-521-45520-6。
• ニプコウ、トビアス編 (1998).書き換え技術と応用, 第9回国際会議, RTA-98 . LNCS. 第1379巻. シュプリンガー
• Nipkow T.、Paulson L.、Wenzel M. (2002). Isabelle/HOL — 高階論理のための証明支援系. Springer.
• Gerwin Klein & Tobias Nipkow (2006). 「Javaライクな言語、仮想マシン、コンパイラのための機械検証モデル」 ACM Transactions on Programming Languages and Systems 28 ( 4): 619– 695. doi : 10.1145/1146809.1146811 .

参考文献

1. ブランシェット、ジャスミン（2021年2月12日）「新編集長からのメッセージ」 Journal of Automated Reasoning . 65 (2): 155. doi : 10.1007/s10817-021-09587-y . hdl : 1871.1/1216cab9-08c1-4d41-8069- aa1735f5786d
2. 略歴
3. 「自動推論への顕著な貢献に対するエルブランド賞」 CADE Inc. 2021年7月14日閲覧。
4. "Tobias Nipkow" .会員. Academia Europaea . 2024年10月3日閲覧。

外部リンク

• ホームページ