Most cited papers in Logic, programming, and type systems
What are the most cited papers in Logic, programming, and type systems?
The most cited paper in Logic, programming, and type systems is "Compilers: Principles, Techniques, and Tools" (Alfred V. Aho, Ravi Sethi, Jeffrey David Ullman, 1986), with 8,166 citations. Next come "Communication and Concurrency" (6,871) and "Z3: An Efficient SMT Solver" (6,516).
Showing 50 of 97 papers. Every paper with more than 1,123 citations is listed.
| # | Paper | ||
|---|---|---|---|
| 1 | Compilers: Principles, Techniques, and Tools Alfred V. Aho, Ravi Sethi, Jeffrey David Ullman | 1986 | 8,166 |
| 2 | Communication and Concurrency Robin Milner | 1989 | 6,871 |
| 3 | Z3: An Efficient SMT Solver Leonardo de Moura, Nikolaj Bjørner · Lecture notes in computer science | 2008 | 6,516 |
| 4 | A Complexity Measure Thomas J. McCabe · IEEE Transactions on Software Engineering | Dec 1976 | 5,923 |
| 5 | The temporal logic of programs Amir Pnueli | Sep 1977 | 5,753 |
| 6 | On observing nondeterminism and concurrency Matthew Hennessy, Robin Milner · Lecture notes in computer science | 1980 | 4,501 |
| 7 | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games Phan Minh Dũng · Artificial Intelligence | Sep 1995 | 4,320 |
| 8 | Linear logic Jean-Yves Girard · Theoretical Computer Science | 1987 | 4,129 |
| 9 | Strips: A new approach to the application of theorem proving to problem solving Richard E. Fikes, Nils J. Nilsson · Artificial Intelligence | Dec 1971 | 4,105 |
| 10 | An axiomatic basis for computer programming C. A. R. Hoare · Communications of the ACM | Oct 1969 | 3,964 |
| 11 | A logic for default reasoning Raymond Reiter · Artificial Intelligence | Apr 1980 | 3,937 |
| 12 | A Machine-Oriented Logic Based on the Resolution Principle John A. Robinson · Journal of the ACM | 1965 | 3,931 |
| 13 | Communicating sequential processes C. A. R. Hoare · Communications of the ACM | 1983 | 3,789 |
| 14 | Automatic verification of finite-state concurrent systems using temporal logic specifications E. M. Clarke, E. Allen Emerson, Aravinda Prasad Sistla · ACM Transactions on Programming Languages and Systems | Apr 1986 | 3,602 |
| 15 | A Temporal Logic of Nested Calls and Returns Rajeev Alur, Kousha Etessami, P. Madhusudan · Lecture notes in computer science | 2004 | 3,339 |
| 16 | On the logic of theory change: Partial meet contraction and revision functions Carlos E. Alchourrón, Peter Gärdenfors, David Makinson · Journal of Symbolic Logic | Jun 1985 | 3,248 |
| 17 | A machine program for theorem-proving Martin D. Davis, George W. Logemann, Donald W. Loveland · Communications of the ACM | Jul 1962 | 3,234 |
| 18 | Symbolic execution and program testing James C. King · Communications of the ACM | Jul 1976 | 3,043 |
| 19 | A calculus of mobile processes, I Robin Milner, Joachim Parrow, David S. Walker · Information and Computation | Sep 1992 | 2,867 |
| 20 | Constructing Induction Rules for Deductive Synthesis Proofs Alan Bundy, Lucas Dixon, Jeremy Gow et al. · Electronic Notes in Theoretical Computer Science | Mar 2006 | 2,818 |
| 21 | The program dependence graph and its use in optimization Jeanne Ferrante, Karl J. Ottenstein, Joe D. Warren · ACM Transactions on Programming Languages and Systems | Jul 1987 | 2,776 |
| 22 | A Computing Procedure for Quantification Theory Martin D. Davis, Hilary Putnam · Journal of the ACM | Jul 1960 | 2,643 |
| 23 | An Extensible SAT-solver Niklas Eén, Niklas Sörensson · Lecture notes in computer science | 2004 | 2,642 |
| 24 | LLVM: A compilation framework for lifelong program analysis & transformation Chris Lattner, Vikram Adve | 10 Jun 2004 | 2,639 |
| 25 | The symbol grounding problem Stevan Harnad · Physica D Nonlinear Phenomena | Jun 1990 | 2,630 |
| 26 | Can programming be liberated from the von Neumann style? John Backus · Communications of the ACM | Aug 1978 | 2,613 |
| 27 | How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs Lamport · IEEE Transactions on Computers | Sep 1979 | 2,537 |
| 28 | The knowledge level Allen Newell · Artificial Intelligence | 1982 | 2,505 |
| 29 | Distributed snapshots K. Mani Chandy, Leslie Lamport · ACM Transactions on Computer Systems | Feb 1985 | 2,449 |
| 30 | Isabelle/HOL: A Proof Assistant for Higher-Order Logic Tobias Nipkow, Markus Wenzel, Lawrence Charles Paulson · Digital Access to Libraries (Université catholique de Louvain (UCL), l'Université de Namur (UNamur) and the Université Saint-Louis (USL-B)) | 2002 | 2,319 |
| 31 | An Algorithm for Subgraph Isomorphism Julian R. Ullmann · Journal of the ACM | 1976 | 2,300 |
| 32 | Types and Programming Languages Benjamin C. Pierce | 2002 | 2,242 |
| 33 | A theory of type polymorphism in programming Robin Milner · Journal of Computer and System Sciences | Dec 1978 | 2,221 |
| 34 | Design and synthesis of synchronization skeletons using branching time temporal logic Edmund M. Clarke, E. Allen Emerson · Lecture notes in computer science | 19 Nov 2005 | 2,198 |
| 35 | Separation logic: a logic for shared mutable data structures John Reynolds | 25 Jun 2003 | 2,172 |
| 36 | Circumscription—A form of non-monotonic reasoning John McCarthy · Artificial Intelligence | Apr 1980 | 2,034 |
| 37 | A Structural Approach to Operational Semantics Gordon D. Plotkin | 2004 | 1,983 |
| 38 | Direct Manipulation: A Step Beyond Programming Languages Shneiderman · Computer | Aug 1983 | 1,929 |
| 39 | Temporal and Modal Logic E. Allen Emerson · Elsevier eBooks | 1990 | 1,913 |
| 40 | The algorithmic analysis of hybrid systems Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs et al. · Theoretical Computer Science | Feb 1995 | 1,889 |
| 41 | Concurrency and automata on infinite sequences David S. Park · Lecture notes in computer science | 22 Nov 2005 | 1,883 |
| 42 | AMPL : a modeling language for mathematical programming Robert Fourer, Brian W. Kernighan | 1993 | 1,870 |
| 43 | Proof-carrying code George C. Necula | 1997 | 1,838 |
| 44 | Results on the propositional μ-calculus Dexter C. Kozen · Theoretical Computer Science | 1983 | 1,825 |
| 45 | A truth maintenance system Jon Doyle · Artificial Intelligence | Nov 1979 | 1,782 |
| 46 | The complexity of satisfiability problems Thomas J. Schaefer | 1978 | 1,769 |
| 47 | Fast Probabilistic Algorithms for Verification of Polynomial Identities Jacob T. Schwartz · Journal of the ACM | Oct 1980 | 1,747 |
| 48 | The Esterel synchronous programming language: design, semantics, implementation Gérard Berry, Georges Gonthier · Science of Computer Programming | Nov 1992 | 1,734 |
| 49 | Notions of computation and monads Eugenio Moggi · Information and Computation | Jul 1991 | 1,716 |
| 50 | Structural equivalence of individuals in social networks François Lorrain, Harrison C. White · Journal of Mathematical Sociology | 1971 | 1,710 |
Citations are OpenAlex's own counts, from its 2026-09-23 snapshot, so the ranking can differ from Google Scholar or Web of Science. A paper is listed for a field when OpenAlex files it under one of the field's topics; retracted papers and papers whose citation count cannot be traced to citing works are left out, and a preprint and the article it became are shown once. Release dates are OpenAlex's: where a source gave only a month or a year, that is what is shown. How the lists are chosen.