Tobias Nipkow (born 1958) is a German computer scientist.
Career
Nipkow received his
Diplom
A ''Diplom'' (, from grc, δίπλωμα ''diploma'') is an academic degree in the German-speaking countries Germany, Austria, and Switzerland and a similarly named degree in some other European countries including Albania, Bulgaria, Belarus ...
(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
Across the many fields concerned with interactivity, including information science, computer science, human-computer interaction, communication, and industrial design, there is little agreement over the meaning of the term "interactivity", but mo ...
and
automatic theorem proving
Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a maj ...
, in particular for the
Isabelle proof assistant; he was the editor of the ''
Journal of Automated Reasoning
The ''Journal of Automated Reasoning'' was established in 1983 by Larry Wos, who was its editor in chief until 1992. It covers research and advances in automated reasoning, mechanical verification of theorems, and other deductions in classical and ...
'' up to January 1, 2021. Moreover, he focuses on
programming language semantics
In programming language theory, semantics is the rigorous mathematical study of the meaning of programming languages. Semantics assigns computational meaning to valid strings in a programming language syntax.
Semantics describes the processe ...
,
type systems and
functional programming.
In 2021 he won the
Herbrand Award The Herbrand Award for Distinguished Contributions to Automated Reasoning is an award given by the Conference on Automated Deduction (CADE), Inc., (although it predates the formal incorporation of CADE) to honour persons or groups for important cont ...
"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