Tobias Nipkow
| Naissance | |
|---|---|
| Nationalité | |
| Domicile | |
| Formation | |
| Activité |
| A travaillé pour | |
|---|---|
| Directeur de thèse |
Cliff Jones (en) |
| Site web |
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, « Unification in Primal Algebras, their Powers and their Varieties », Journal of the ACM, vol. 37, no 4, , 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), , 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), .
- Franz Baader et Tobias Nipkow, Term Rewriting and All That, Cambridge University Press, (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 » (no 2283), , 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, , p. 619–695 (DOI 10.1145/1146809.1146811)
- 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]
- (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) « Tobias Nipkow », sur le site du Mathematics Genealogy Project
- 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).
- Page sur l'université.
- « Herbrand Award for Distinguished Contributions to Automated Reasoning », CADE Inc (consulté le ).
Liens externes[modifier | modifier le code]
- (en) Site officiel
- Ressources relatives à la recherche :
