| 2006 |
|---|
| 25 | EE | Robert S. Boyer,
Warren A. Hunt Jr.:
Function memoization and unique object representation for ACL2 functions.
ACL2 2006: 81-89 |
| 2005 |
|---|
| 24 | EE | Robert S. Boyer,
Warren A. Hunt Jr.,
Serita M. Nelesen:
A Compressed Format for Collections of Phylogenetic Trees and Improved Consensus Performance.
WABI 2005: 353-364 |
| 23 | EE | Robert S. Boyer,
Wilfred J. Legato,
Victor W. Marek:
Toward Automating the Discovery of Decreasing Measures.
J. Autom. Reasoning 35(4): 355-371 (2005) |
| 2002 |
|---|
| 22 | EE | Robert S. Boyer,
J. Strother Moore:
Single-Threaded Objects in ACL2.
PADL 2002: 9-27 |
| 21 | EE | Robert S. Boyer,
W. H. J. Feijen,
David Gries,
C. A. R. Hoare,
Jayadev Misra,
J. Moore,
H. Richards:
In memoriam: Edsger W. Dijkstra 1930-2002.
Commun. ACM 45(10): 21-22 (2002) |
| 1996 |
|---|
| 20 | | Michael Ballantyne,
Robert S. Boyer,
Larry M. Hines:
Woody Bledsoe - His Life and Legacy.
AI Magazine 17(1): 7-20 (1996) |
| 19 | EE | Robert S. Boyer,
Yuan Yu:
Automated Proofs of Object Code for a Widely Used Microprocessor.
J. ACM 43(1): 166-192 (1996) |
| 1994 |
|---|
| 18 | | Robert S. Boyer:
Panel Discussion: A Mechanically Proof-Checked Encyclopedia of Mathematics: Should We Build One? Can We?
CADE 1994: 237 |
| 1992 |
|---|
| 17 | | Robert S. Boyer,
Yuan Yu:
Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor.
CADE 1992: 416-430 |
| 1991 |
|---|
| 16 | | Anne Olivia Boyer,
Robert S. Boyer:
A Biographical Sketch of W. W. Bledsoe.
Automated Reasoning: Essays in Honor of Woody Bledsoe 1991: 1-30 |
| 15 | | Robert S. Boyer,
J. Strother Moore:
MJRTY: A Fast Majority Vote Algorithm.
Automated Reasoning: Essays in Honor of Woody Bledsoe 1991: 105-118 |
| 1990 |
|---|
| 14 | | Robert S. Boyer,
J. Strother Moore:
A Theorem Prover for a Computational Logic.
CADE 1990: 1-15 |
| 1989 |
|---|
| 13 | EE | Hassan Aït-Kaci,
Robert S. Boyer,
Patrick Lincoln,
Roger Nasr:
Efficient Implementation of Lattice Operations.
ACM Trans. Program. Lang. Syst. 11(1): 115-146 (1989) |
| 1988 |
|---|
| 12 | | Robert S. Boyer,
J. Strother Moore:
The Addition of Bounded Quantification and Partial Functions to A Computational Logic and Its Theorem Prover.
J. Autom. Reasoning 4(2): 117-172 (1988) |
| 1986 |
|---|
| 11 | | Robert S. Boyer,
J. Strother Moore:
Overview of a Theorem-Prover for A Computational Logic.
CADE 1986: 675-678 |
| 10 | | Robert S. Boyer,
Ewing L. Lusk,
William McCune,
Ross A. Overbeek,
Mark E. Stickel,
Larry Wos:
Set Theory in First-Order Logic: Clauses for Gödel's Axioms.
J. Autom. Reasoning 2(3): 287-327 (1986) |
| 1985 |
|---|
| 9 | | Robert S. Boyer,
J. Strother Moore:
Program Verification.
J. Autom. Reasoning 1(1): 17-23 (1985) |
| 1984 |
|---|
| 8 | EE | Robert S. Boyer,
J. Strother Moore:
A Mechanical Proof of the Unsolvability of the Halting Problem.
J. ACM 31(3): 441-458 (1984) |
| 1977 |
|---|
| 7 | | Robert S. Boyer,
J. Strother Moore:
A Lemma Driven Automatic Theorem Prover for Recursive Function Theory.
IJCAI 1977: 511-519 |
| 6 | | Robert S. Boyer,
J. Strother Moore:
A Fast String Searching Algorithm.
Commun. ACM 20(10): 762-772 (1977) |
| 1976 |
|---|
| 5 | | Robert S. Boyer,
J. Strother Moore,
Robert E. Shostak:
Primitive Recursive Program Transformations.
POPL 1976: 171-174 |
| 1975 |
|---|
| 4 | EE | Robert S. Boyer,
J. Strother Moore:
Proving Theorems about LISP Functions.
J. ACM 22(1): 129-144 (1975) |
| 1973 |
|---|
| 3 | | Robert S. Boyer,
J. Strother Moore:
Proving Theorems about LISP Functions.
IJCAI 1973: 486-493 |
| 1972 |
|---|
| 2 | | W. W. Bledsoe,
Robert S. Boyer,
William H. Henneman:
Computer Proofs of Limit Theorems.
Artif. Intell. 3(1-3): 27-60 (1972) |
| 1971 |
|---|
| 1 | | W. W. Bledsoe,
Robert S. Boyer,
William H. Henneman:
Computer Proofs of Limit Theorems.
IJCAI 1971: 586-600 |
