Elamur Research⌕
☰
home / authors / Tobias Nipkow

Tobias Nipkow

Tobias Nipkow has 2 papers in our library, in 2008–2015, most of them on Reasoning; often with Cezary Kaliszyk, John Harrison, Lawrence C. Paulson.

2 papers in our library · 2008–2015

OpenAlex · ORCID · Wikidata · h-index 46 · 426 works · 12,164 citations OpenAlex, 2026-10-14

📄 2 works in our library · 🔗 Cited 51 times in our library · ⭐ Paper Stars ranking: #6083

The profile is the library's match of the name; two people with one name are not always told apart.

Elsewhere: Google Scholar · Semantic Scholar · dblp · ACL Anthology

 Affiliations

🎓Technical University of MunichMunich · Germany1992–2026 · 182 papersEmploymentcurrent🎓University of CambridgeCambridge · United Kingdom1989–2002 · 11 papers🎓University of ManchesterManchester · United Kingdom1986–2006 · 5 papersEducation🎓Massachusetts Institute of TechnologyCambridge · United States1988–1989 · 5 papers🎓Technische Universität DarmstadtDarmstadt · Germany2005–2006 · 2 papersEducation🎓Ludwig-Maximilians-Universität MünchenMunich · Germany1993–1994 · 2 papers🎓University of LondonLondon · United Kingdom1989–1990 · 2 papers

From the bylines of their papers (OpenAlex, 2026-10-14), ORCID and Wikidata; institutions on papers are matched by machine. 1 more institution on single bylines are not listed.

 Fields, topics and concepts

Of its works in our library, with the number of works on each.

📚 Shelves 6The field of science this work belongs to (OpenAlex fields).Computer Science · 2 worksArtificial Intelligence · 2 worksComputational Theory and Mathematics · 1 workMathematics · 1 workAlgebra and Number Theory · 1 workNumerical Analysis · 1 work

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1 work

 Works by year

2010s

20151 paper

2000s

20081 paper

 Papers

The most cited first (OpenAlex and our library).

  1. The Isabelle Framework (2008 · 183 citations)
    Note: the supplied text is not "The Isabelle Framework" (Wenzel, Paulson, Nipkow). It is "A Compiled Implementation of Normalization by Evaluation" by Klaus Aehlig, Florian Haftmann and Tobias Nipkow, and this summary covers that text.
  2. A formal proof of the Kepler conjecture (2015 · 79 citations)
    The Kepler conjecture claims that no arrangement of equal balls in three-dimensional space is denser than the face-centered cubic packing, whose density is π/√18 (about 0.74).

 Co-authors here

3 co-authors with a page, the most papers together first.

Venues

Where their works here were published, the most works first, with the editions of those that have a page.

 Cited by

Papers of our library cite their works 51 times (of the 149,439 papers whose bibliographies we read); 31 citing papers with a page here →.

Updated

This page in Markdown → https://md.research.elamur.ai/free/en/authors/tobias-nipkow/