Tobias Nipkow Explained

Tobias Nipkow
Birth Date:	1958
Workplaces:	MIT, Cambridge University, TU Munich
Thesis Title:	Behavioural Implementation Concepts for Nondeterministic Data Types
Thesis Url:	https://www.worldcat.org/oclc/18002367
Thesis Year:	1987
Doctoral Advisor:	Cliff B. Jones
Known For:	Isabelle proof assistant
Spouses:	)-->
Partners:	)-->

Tobias Nipkow (born 1958) is a German computer scientist.

Career

Nipkow received his Diplom (MSc) in computer science from the Department of Computer Science of the Technische Hochschule Darmstadt in 1982, and his Ph.D. from the University of Manchester in 1987.

He worked at MIT from 1987, changed to Cambridge University in 1989, and to Technical University Munich in 1992, where he was appointed professor for programming theory.

He is chair of the Logic and Verification group since 2011.

He is known for his work in interactive and automatic theorem proving, in particular for the Isabelle proof assistant; he was the editor of the Journal of Automated Reasoning up to January 1, 2021.^[1] Moreover, he focuses on programming language semantics, type systems and functional programming.^[2]

In 2021 he won the Herbrand Award "in recognition of his leadership in developing Isabelle and related tools, resulting in key contributions to the foundations, automation, and use of proof assistants in a wide range of applications, as well as his successful efforts in increasing the visibility of automated reasoning".^[3]

Selected publications

• Book: Martin, U. . Nipkow, T. . amp . Unification in Boolean Rings . Jörg H. Siekmann . Proc. 8th Conference on Automated Deduction . Springer . . 230 . 506–513 . 1986 . Conference on Automated Deduction .
• Ph.D. thesis . Tobias Nipkow . Behavioural Implementation Concepts for Nondeterministic Data Types . University of Manchester . Computer Science Dept. Report . UMCS-87-5-3 . 1987 .
• Book: Nipkow, T. . Combining Matching Algorithms: The Rectangular Case . 343–358 . 1989 . Nachum Dershowitz. Rewriting Techniques and Applications, 3rd Int. Conf., RTA-89 . LNCS . 355 . Springer. Rewriting Techniques and Applications .
• Tobias Nipkow . Unification in Primal Algebras, their Powers and their Varieties . . 37 . 4 . 742–776 . 1990 . 10.1145/96559.96569. 14940917 . free .
• Book: Nipkow, T. . Qian, Z. . amp . Modular Higher-Order E-Unification . 200–214 . 1991 . Book, Ronald V. . Rewriting Techniques and Applications, 4th Int. Conf., RTA-91 . LNCS . 488 . Springer.
• Book: Tobias Nipkow . Higher-Order Critical Pairs . Proc. 6th IEEE Symposium on Logic in Computer Science . 342–349 . 1991 . IEEE Symposium on Logic in Computer Science .
• Book: Nipkow, T. . Higher-Order Rewrite Systems (invited lecture) . 256 . 1995 . Hsiang, Jieh . 6th Int. Conf. on Rewriting Techniques and Applications (RTA) . LNCS . 914 . Springer.
• Book: Franz Baader and Tobias Nipkow . Term Rewriting and All That . Cambridge . Cambridge University Press . 978-0-521-45520-6 . 1998 .
• Book: 1998 . Nipkow, Tobias . Rewriting Techniques and Applications, 9th Int. Conf., RTA-98 . LNCS . 1379 . Springer .
• Book: Nipkow T. and Paulson L. and Wenzel M. . Isabelle/HOL - A Proof Assistant for Higher-Order Logic . Springer . 2002 . Isabelle (proof assistant) .
• Gerwin Klein . Tobias Nipkow . amp . A Machine-Checked Model for a Java-Like Language, Virtual Machine and Compiler . . 28 . 4 . 619–695 . 2006 . 10.1145/1146809.1146811. free .

External links

• Home page

Notes and References

1. Blanchette . Jasmin . Message from the New Editor-in-Chief . Journal of Automated Reasoning . 2. 12 February 2021. 65 . 155 . 10.1007/s10817-021-09587-y . free . 1871.1/1216cab9-08c1-4d41-8069-aa1735f5786d . free .
2. http://www.professoren.tum.de/nipkow-tobias Brief vita
3. Web site: Herbrand Award for Distinguished Contributions to Automated Reasoning . CADE Inc. 14 July 2021.