Elamur Research⌕
☰
home / authors / Lawrence C. Paulson

Lawrence C. Paulson

Lawrence C. Paulson has 4 papers in our library, in 1990–2020, most of them on Reasoning, Evaluation & benchmarks; often with Cezary Kaliszyk, Josef Urban, Lei Yu.

4 papers in our library · 1990–2020

OpenAlex · ORCID · Wikidata · h-index 45 · 283 works · 10,329 citations OpenAlex, 2026-10-14

📄 4 works in our library · 🔗 Cited 95 times in our library · ⭐ Paper Stars ranking: #5047

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

🎓University of CambridgeCambridge · United Kingdom1982–2026 · 197 papersEmployment since 1983 · Emeritus Professor of Computational Logic, Computer Laboratorycurrent🏢AmazonLondon · United Kingdom2026 · 1 papercurrent🎓Technical University of MunichMunich · Germany2018 · 1 paperEmployment🎓Stanford UniversityStanford · United States1977–1982 · 1 paperEducation 1977–1982 · PhD, Computer Science🎓California Institute of TechnologyPasadena · United States1973–1977Education 1973–1977 · BS, Mathematics

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 5The field of science this work belongs to (OpenAlex fields).Computer Science · 4 worksArtificial Intelligence · 4 worksComputational Theory and Mathematics · 4 worksArts and Humanities · 1 workLanguage and Linguistics · 1 work

🧭 Topics 2Research subjects and languages the work is about.Reasoning · 4 worksEvaluation & benchmarks · 1 work

💡 Concepts 1Key ideas and methods explained on our concept pages.Lemma · 1 work

 Works by year

2020s

20201 paper

2010s

20161 paper

2000s

20081 paper

1990s

19901 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. Hammering towards QED (2016 · 127 citations)
    This survey covers "hammers," tools that let users of proof assistants prove hard lemmas automatically. The user does not have to script the proof search by hand. The tools draw on very large formal libraries, and the name comes from Sledgehammer for Isabelle and HOLyHammer for HOL Light.
  3. IsarStep: a Benchmark for High-level Mathematical Reasoning (2020 · 43 citations)
    Most neural work on mathematical reasoning has targeted narrow, synthetic problems such as arithmetic or symbolic integration, which use very small vocabularies.
  4. Isabelle: The Next 700 Theorem Provers (1990 · 40 citations)
    The paper surveys Isabelle, a generic interactive theorem prover. Rather than building a separate LCF-style system for each new logic, Isabelle tackles problems common to all logics once, so that each logic only needs its own specific parts. Paulson tells the system's history, starting from Milner's Edinburgh LCF…

 Co-authors here

6 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 95 times (of the 149,439 papers whose bibliographies we read); 57 citing papers with a page here →.

Updated

This page in Markdown → https://md.research.elamur.ai/free/en/authors/lawrence-c-paulson/