Tobias Nipkow | |
---|---|

Born | 1958 |

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 |

Website | www21 |

**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] }

- 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". In Nachum 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. and Paulson 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 .

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

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.

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

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

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

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

- ↑ 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 . - ↑ Brief vita
- ↑ "Herbrand Award for Distinguished Contributions to Automated Reasoning". CADE Inc. Retrieved 14 July 2021.

This page is based on this Wikipedia article

Text is available under the CC BY-SA 4.0 license; additional terms may apply.

Images, videos and audio are available under their respective licenses.

Text is available under the CC BY-SA 4.0 license; additional terms may apply.

Images, videos and audio are available under their respective licenses.