Tobias Nipkow (born 1958) is a German computer scientist.
Career
Nipkow received his
Diplom (MSc) in
computer science
Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to practical disciplines (includi ...
from the
Department of Computer Science of the
Technische Hochschule Darmstadt in 1982, and his Ph.D. from the
University of Manchester
, mottoeng = Knowledge, Wisdom, Humanity
, established = 2004 – University of Manchester Predecessor institutions: 1956 – UMIST (as university college; university 1994) 1904 – Victoria University of Manchester 1880 – Victoria Univ ...
in 1987.
He worked at
MIT
The Massachusetts Institute of Technology (MIT) is a private land-grant research university in Cambridge, Massachusetts. Established in 1861, MIT has played a key role in the development of modern technology and science, and is one of the m ...
from 1987, changed to
Cambridge University
The University of Cambridge is a Public university, public collegiate university, collegiate research university in Cambridge, England. Founded in 1209 and granted a royal charter by Henry III of England, Henry III in 1231, Cambridge is the world' ...
in 1989, and to
Technical University Munich
The Technical University of Munich (TUM or TU Munich; german: Technische Universität München) is a public research university in Munich, Germany. It specializes in engineering, technology, medicine, and applied and natural sciences.
Establis ...
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
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 withou ...
; he was the editor of the ''
Journal of Automated Reasoning'' up to January 1, 2021. Moreover, he focuses on
programming language semantics,
type systems and
functional programming
In computer science, functional programming is a programming paradigm where programs are constructed by applying and composing functions. It is a declarative programming paradigm in which function definitions are trees of expressions that ...
.
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".
Selected publications
*
*
*
*
*
*
*
*
*
*
*
References
External links
Home page
German computer scientists
Theoretical computer scientists
Academic staff of the Technical University of Munich
1958 births
Living people
Technische Universität Darmstadt alumni
{{compu-scientist-stub