# Tobias Nipkow

Tobias Nipkow est un informaticien allemand né en 1958.

## Carrière

Nipkow obtient son diplôme en informatique au département d'informatique de la Technische Hochschule Darmstadt en 1982, et son doctorat à l'université de Manchester en 1987.
Il travaille au Massachusetts Institute of Technology à partir de 1987, puis à l'université de Cambridge en 1989 et à l'université technique de Munich en 1992, où est nommé professeur en théorie de la programmation. Il y dirige le groupe « Logique et Vérification » depuis 2011.

## Recherche

Nipkow est connu pour ses travaux sur la démonstration interactive et la démonstration automatique de théorèmes, en particulier pour l'assistant de preuve Isabelle ; il est également rédacteur en chef du Journal of Automated Reasoning jusqu'au 1er janvier 2021. Plus generalement, Nipkow travaille sur la sémantique des langages de programmation, les systèmes de types et la programmation fonctionnelle

## Récompenses

En 2021, Nipkow est lauréat du prix Herbrand « en reconnaissance de son leadership dans le développement d'Isabelle et des outils associés, résultant en des contributions clés aux fondations, à l'automatisation et à l'utilisation d'assistants de preuve dans un large éventail d'applications, ainsi que ses efforts réussis pour accroître la visibilité du raisonnement automatisé".

## Publications (sélection)

* Martin, U. et Tobias Nipkow, Proc. 8th Conference on Automated Deduction, vol. 230, Springer, coll. « Lecture Notes in Computer Science », 1986, « Unification in Boolean Rings », p. 506–513.
* Tobias Nipkow, Behavioural Implementation Concepts for Nondeterministic Data Types, vol. UMCS-87-5-3 (Ph.D. thesis), University of Manchester, coll. « Computer Science Dept. Report », 1987
* Tobias Nipkow, « Combining Matching Algorithms: The Rectangular Case », Rewriting Techniques and Applications, 3rd Int. Conf., RTA-89, Springer Lecture Notes in Computer Science (n° 355),‎ 1989, p. 343–358
* Tobias Nipkow, « Unification in Primal Algebras, their Powers and their Varieties », Journal of the ACM, vol. 37, n$^o$ 4,‎ 1990, p. 742–776 (DOI 10.1145/96559.96569, S2CID 14940917)
* Tobias Nipkow et Z. Qian, « Modular Higher-Order E-Unification », Rewriting Techniques and Applications, 4th Int. Conf., RTA-91, Lecture Notes in Computer Science (n° 488),‎ 1991, p. 200–214
* Tobias Nipkow, Proc. 6th IEEE Symposium on Logic in Computer Science, 1991, 342–349 p., « Higher-Order Critical Pairs »
* Tobias Nipkow, « Higher-Order Rewrite Systems (invited lecture) », 6th Int. Conf. on Rewriting Techniques and Applications (RTA), Springer Lecture Notes in Computer Science (n° 914),‎ 1995.
* Franz Baader et Tobias Nipkow, Term Rewriting and All That, Cambridge University Press, 1999 (ISBN 978-0-521-45520-6)
* Tobias Nipkow, Lawrence C. Paulson et Markus Wenzel, Isabelle/HOL: a proof assistant for higher-order logic, Springer, coll. « Lecture Notes in Computer Science » (n$^o$ 2283), 2002, xiv + 226 (ISBN 978-3-540-43376-7)
* Gerwin Klein et Tobias Nipkow, « A Machine-Checked Model for a Java-Like Language, Virtual Machine and Compiler », ACM Transactions on Programming Languages and Systems, vol. 28,‎ 2006, p. 619–695 (DOI 10.1145/1146809.1146811)
* Tobias Nipkow et Gerwin Klein, Concrete semantics: with Isabelle/HOL, Springer, 2014, xiii+ 298 (ISBN 978-3-319-10541-3)
* Thomas Hales, Mark Adams, Gertrud Bauer et Tat Dat Dang et. al., « A formal proof of the Kepler conjecture », Forum of Mathematics, Pi, vol. 5,‎ janvier 2017, e2 (DOI 10.1017/fmp.2017.1, lire en ligne)