トビアス・ニプコウ

トビアス・ニプコウ（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。 
• Tobias Nipkow (1990). "原始代数、その冪、および多様体における統一性" . Journal of the 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。 
• Tobias Nipkow (1991). 「高階クリティカルペア」.第 6 回 IEEE コンピュータサイエンスにおける論理シンポジウム議事録. pp. 342–349 . 
• Nipkow, T. (1995). 「高階書き換えシステム（招待講演）」. Hsiang, Jieh (編).第 6 回書き換え技術と応用に関する国際会議 (RTA) . LNCS. Vol.  914. Springer. p.  256.
• フランツ・バーダー、トビアス・ニプコウ（1998）。用語書き換えとその他諸々。ケンブリッジ：ケンブリッジ大学出版局。ISBN 978-0-521-45520-6。
• Nipkow, Tobias 編 (1998). Rewriting Techniques and Applications, 9th Int. Conf., RTA-98 . LNCS. Vol.  1379. Springer.
• 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 .

• ホームページ