Tobias Nipkow

Last updated
Tobias Nipkow
Known for Isabelle proof assistant
Scientific career
Institutions MIT, Cambridge University, TU Munich
Thesis Behavioural Implementation Concepts for Nondeterministic Data Types  (1987)
Doctoral advisor Cliff B. Jones

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



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

Related Research Articles

Automated theorem proving is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major impetus for the development of computer science.

In logic and computer science, unification is an algorithmic process of solving equations between symbolic expressions.

<span class="mw-page-title-main">Isabelle (proof assistant)</span> Higher-order logic (HOL) automated theorem prover

The Isabelle automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As an LCF-style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring — yet supporting — explicit proof objects.

In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. Such methods may be achieved by rewriting systems. In their most basic form, they consist of a set of objects, plus relations on how to transform those objects.

<span class="mw-page-title-main">Henk Barendregt</span> Dutch logician (born 1947)

Hendrik Pieter (Henk) Barendregt is a Dutch logician, known for his work in lambda calculus and type theory.

Franz Baader is a German computer scientist at Dresden University of Technology.

In mathematics, in the theory of rewriting systems, Newman's lemma, also commonly called the diamond lemma, states that a terminating abstract rewriting system (ARS), that is, one in which there are no infinite reduction sequences, is confluent if it is locally confluent. In fact a terminating ARS is confluent precisely when it is locally confluent.

Rewriting Techniques and Applications (RTA) is an annual international academic conference on the topic of rewriting. It covers all aspects of rewriting, including termination, equational reasoning, theorem proving, higher-order rewriting, unification and the lambda calculus. The conference consists of peer-reviewed papers with the proceedings published by Springer in the LNCS series until 2009, and since then in the LIPIcs series published by the Leibniz-Zentrum für Informatik. Several rewriting-related workshops are also affiliated with RTA.

In computer science, termination analysis is program analysis which attempts to determine whether the evaluation of a given program halts for each input. This means to determine whether the input program computes a total function.

<span class="mw-page-title-main">John Alan Robinson</span> American computer scientist

John Alan Robinson was a philosopher, mathematician, and computer scientist. He was a professor emeritus at Syracuse University.

Gérard Pierre Huet is a French computer scientist, linguist and mathematician. He is senior research director at INRIA and mostly known for his major and seminal contributions to type theory, programming language theory and to the theory of computation.

Jan Willem Klop is a professor of applied logic at Vrije Universiteit in Amsterdam. He holds a Ph.D. in mathematical logic from Utrecht University. Klop is known for his work on the Algebra of Communicating Processes, co-author of TeReSe and his fixed point combinator

Anti-unification is the process of constructing a generalization common to two given symbolic expressions. As in unification, several frameworks are distinguished depending on which expressions are allowed, and which expressions are considered equal. If variables representing functions are allowed in an expression, the process is called "higher-order anti-unification", otherwise "first-order anti-unification". If the generalization is required to have an instance literally equal to each input expression, the process is called "syntactical anti-unification", otherwise "E-anti-unification", or "anti-unification modulo theory".

Dis-unification, in computer science and logic, is an algorithmic process of solving inequations between symbolic expressions.

<span class="mw-page-title-main">Radhia Cousot</span> Inventor of abstract interpretation

Radhia Cousot was a French computer scientist known for inventing abstract interpretation.

<span class="mw-page-title-main">Jean-Pierre Jouannaud</span> French computer scientist (born 1947)

Jean-Pierre Jouannaud is a French computer scientist, known for his work in the area of term rewriting.

Nachum Dershowitz is an Israeli computer scientist, known e.g. for the Dershowitz–Manna ordering and the multiset path ordering used to prove termination of term rewrite systems.

Wayne Snyder is an associate professor at Boston University known for his work in E-unification theory.

In computer science, interference freedom is a technique for proving partial correctness of concurrent programs with shared variables. Hoare logic had been introduced earlier to prove correctness of sequential programs. In her PhD thesis under advisor David Gries, Susan Owicki extended this work to apply to concurrent programs.

Deepak Kapur is a Distinguished Professor in the Department of Computer Science at the University of New Mexico.


  1. Blanchette, Jasmin (12 February 2021). "Message from the New Editor-in-Chief". Journal of Automated Reasoning. 65 (2): 155. doi: 10.1007/s10817-021-09587-y .
  2. Brief vita
  3. "Herbrand Award for Distinguished Contributions to Automated Reasoning". CADE Inc. Retrieved 14 July 2021.