Siddhesh Joshi (Editor)

Tobias Nipkow

Updated on
Edit
Like
Comment
Share on FacebookTweet on TwitterShare on LinkedInShare on Reddit
Name
  
Tobias Nipkow

Residence
  
Munich, Germany


Known for
  
Isabelle

Doctoral advisor
  
Cliff Jones

Tobias Nipkow www21intumdenipkowichjpg

Institutions
  
MIT, Cambridge University, TU Munich

Thesis
  
Behavioural Implementation Concepts for Nondeterministic Data Types (1987)

Doctoral students
  
Gertrud Bauer, Stefan Berghofer, Amine Chaieb, Florian Haftmann, Johannes Holzl, Gerwin Klein, Alexander Krauss, Olaf Muller, Dieter Nazareth, Steven Obua, Christian Prehofer, Leonor Prensa-Nieto, Franz Regensburger, Norbert Schirmer, Konrad Slind, David von Oheimb, Tjark Weber, Markus Wenzel, Martin Wildmoser

Books
  
Concrete Semantics: With Isabelle/HOL

Tobias Nipkow (born 1958) is a German computer scientist. He received his Diplom (MSc) in computer science from 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.

Tobias Nipkow Tobias Nipkow

He is known for his work in interactive and automatic theorem proving, in particular for the Isabelle proof assistant; he is the editor of the Journal of Automated Reasoning. Moreover, he focuses on programming language semantics, type systems and functional programming.

Selected publications

  • Martin, U. & Nipkow, T. (1986). "Unification in Boolean Rings". In Jörg H. Siekmann. Proc. 8th Conference on Automated Deduction. LNCS. 230. Springer. pp. 506–513. 
  • Tobias Nipkow (1987). Behavioural Implementation Concepts for Nondeterministic Data Types (Ph.D. thesis). Computer Science Dept. Report. UMCS-87-5-3. University of Manchester. 
  • Nipkow, T. (1989). "Combining Matching Algorithms: The Rectangular Case". In Nachum Dershowitz. Rewriting Techniques and Applications, 3rd Int. Conf., RTA-89. LNCS. 355. Springer. pp. 343–358. 
  • Tobias Nipkow (1990). "Unification in Primal Algebras, their Powers and their Varieties". Journal of the ACM. 37: 742–776. doi:10.1145/96559.96569. 
  • Nipkow, T. & Qian, Z. (1991). "Modular Higher-Order E-Unification". In Book, Ronald V. Rewriting Techniques and Applications, 4th Int. Conf., RTA-91. LNCS. 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. 6th Int. Conf. on Rewriting Techniques and Applications (RTA). LNCS. 914. Springer. p. 256. 
  • Franz Baader and Tobias Nipkow (1998). Term Rewriting and All That. Cambridge: Cambridge University Press. ISBN 0-521-45520-0. 
  • Nipkow, Tobias, ed. (1998). Rewriting Techniques and Applications, 9th Int. Conf., RTA-98. LNCS. 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". TOPLAS. 28 (4): 619–695. doi:10.1145/1146809.1146811. 

    • References

    Tobias Nipkow Wikipedia
    (Text) CC BY-SA


    Similar Topics