Tobias Nipkow

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[1].

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.

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 1^er janvier 2021[2]. Plus generalement, Nipkow travaille sur la sémantique des langages de programmation, les systèmes de types et la programmation fonctionnelle[3]

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é"[4].

• 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)

• (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Tobias Nipkow » (voir la liste des auteurs).

• (en) Site officiel
• Ressources relatives à la recherche :
  • Digital Bibliography & Library Project
  • Google Scholar
  • Mathematics Genealogy Project
• Notices d'autorité :

  • VIAF
  • ISNI
  • IdRef
  • LCCN
  • GND
  • Belgique
  • Pays-Bas
  • Israël
  • NUKAT
  • Tchéquie
  • WorldCat

• Portail de l’Allemagne
• Portail de l’informatique