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

Nipkow received hisDiplom (MSc) incomputer science from theDepartment of Computer Science of theTechnische Hochschule Darmstadt in 1982, and his Ph.D. from theUniversity of Manchester in 1987.

He worked atMIT from 1987, changed toCambridge University in 1989, and toTechnical University Munich in 1992, where he was appointed professor forprogramming theory.

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

He is known for his work ininteractive andautomatic theorem proving, in particular for theIsabelle proof assistant; he was the editor of theJournal of Automated Reasoning up to January 1, 2021.^[1] Moreover, he focuses onprogramming language semantics,type systems andfunctional programming.^[2]

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

In 2022, he was elected a member of theAcademia Europaea.^[4]

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

• Home page

• German theoretical computer scientists
• Academic staff of the Technical University of Munich
• Members of Academia Europaea
• 1958 births
• Living people
• Technische Universität Darmstadt alumni
• Computer scientist stubs

• Articles with short description
• Short description is different from Wikidata
• Articles with hCards
• CS1: long volume value
• All stub articles