| Uniform proofs as a foundation for logic programming D Miller, G Nadathur, F Pfenning, A Scedrov Annals of Pure and Applied logic 51 (1-2), 125-157, 1991 | 922 | 1991 |
| An overview of λProlog D Miller, G Nadathur Proc. of the 5th Int. Conf. on Logic Programming, 1988 | 639* | 1988 |
| Higher-order logic programming DA Miller, G Nadathur International Conference on Logic Programming, 448-462, 1986 | 265 | 1986 |
| Programming with higher-order logic D Miller, G Nadathur Cambridge University Press, 2012 | 244 | 2012 |
| A logic programming approach to manipulating formulas and programs D Miller, G Nadathur University of Pennsylvania. Moore School of Electrical Engineering …, 1987 | 167 | 1987 |
| Higher-order unification and matching G Dowek Handbook of automated reasoning, 1009-1062, 2001 | 156 | 2001 |
| Higher-order logic programming G Nadathur, D Miller Handbook of logic in artificial intelligence and logic programming 5, 499-590, 1998 | 156 | 1998 |
| Higher-order Horn clauses G Nadathur, D Miller Journal of the ACM (JACM) 37 (4), 777-814, 1990 | 141 | 1990 |
| Abella: A system for reasoning about relational specifications D Baelde, K Chaudhuri, A Gacek, D Miller, G Nadathur, A Tiu, Y Wang Journal of formalized reasoning 7 (2), 1-89, 2014 | 117 | 2014 |
| System description: Teyjus—A compiler and abstract machine based implementation of λProlog H Ganzinger, G Nadathur, DJ Mitchell Automated Deduction—CADE-16: 16th International Conference on Automated …, 1999 | 112 | 1999 |
| A higher-order logic as the basis for logic programming G Nadathur University of Pennsylvania, 1987 | 107 | 1987 |
| Some uses of higher-order logic in computational linguistics DA Miller, G Nadathur 24th Annual Meeting of the Association for Computational Linguistics, 247-256, 1986 | 94 | 1986 |
| The Bedwyr system for model checking over syntactic expressions D Baelde, A Gacek, D Miller, G Nadathur, A Tiu Automated Deduction–CADE-21: 21st International Conference on Automated …, 2007 | 93 | 2007 |
| HEREDITARY HARROP FORMULAS AND UNIFORM PROOF SYSTEMS. D Miller, G Nadathur, A Scedrov Unknown Host Publication Title, 98-105, 1987 | 85 | 1987 |
| A notation for lambda terms a generalization of environments G Nadathur, DS Wilson Theoretical Computer Science 198 (1-2), 49-98, 1998 | 77* | 1998 |
| A proof procedure for the logic of hereditary Harrop formulas G Nadathur Journal of Automated Reasoning 11, 115-145, 1993 | 72 | 1993 |
| A fine-grained notation for lambda terms and its use in intensional operations G Nadathur Journal of Functional and Logic Programming 2, 1999, 1999 | 71* | 1999 |
| A two-level logic approach to reasoning about computations A Gacek, D Miller, G Nadathur Journal of Automated Reasoning 49 (2), 241-273, 2012 | 67 | 2012 |
| Combining generic judgments with recursive definitions A Gacek, D Miller, G Nadathur 2008 23rd Annual IEEE Symposium on Logic in Computer Science, 33-44, 2008 | 67 | 2008 |
| Nominal abstraction A Gacek, D Miller, G Nadathur Information and Computation 209 (1), 48-73, 2011 | 65 | 2011 |
Dale MillerInria-Saclay and LIX, Ecole PolytechniqueVerified email at inria.fr
