Tobias Nipkow

Tobias Nipkow
une illustration sous licence libre serait bienvenue
Biographie
Naissance
Nationalité
Domicile
Formation
Activité
Autres informations
A travaillé pour
Membre de
Directeur de thèse
Cliff Jones (en)Voir et modifier les données sur Wikidata
Site web
Œuvres principales

modifier - modifier le code - modifier WikidataDocumentation du modèle

Tobias Nipkow est un informaticien allemand né en 1958.

Carrière

[modifier | modifier le code]

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.

Recherche

[modifier | modifier le code]

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

Récompenses

[modifier | modifier le code]

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

Publications (sélection)

[modifier | modifier le code]
  • Martin, U. et Tobias Nipkow, Proc. 8th Conference on Automated Deduction, vol. 230, Springer, coll. « Lecture Notes in Computer Science », , « 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 »,
  • 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),‎ , p. 343–358
  • 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),‎ , p. 200–214
  • Tobias Nipkow, Proc. 6th IEEE Symposium on Logic in Computer Science, , 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),‎ .
  • Tobias Nipkow, Lawrence C. Paulson et Markus Wenzel, Isabelle/HOL: a proof assistant for higher-order logic, Springer, coll. « Lecture Notes in Computer Science » (no 2283), , xiv + 226 (ISBN 978-3-540-43376-7)
  • Tobias Nipkow et Gerwin Klein, Concrete semantics: with Isabelle/HOL, Springer, , 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,‎ , e2 (DOI 10.1017/fmp.2017.1, lire en ligne)

Notes et références

[modifier | modifier le code]
  1. ↑ (en) « Tobias Nipkow », sur le site du Mathematics Genealogy Project
  2. ↑ Jasmin Blanchette, « Message from the New Editor-in-Chief », Journal of Automated Reasoning, vol. 65, no 2,‎ , p. 155 (DOI 10.1007/s10817-021-09587-y).
  3. ↑ Page sur l'université.
  4. ↑ « Herbrand Award for Distinguished Contributions to Automated Reasoning », CADE Inc (consulté le ).

Liens externes

[modifier | modifier le code]