`Travelled to:`

3 × USA

`Collaborated with:`

J.S.Moore Y.Yu R.E.Shostak

`Talks about:`

theorem (2) program (2) prover (2) comput (2) logic (2) microprocessor (1) transform (1) overview (1) commerci (1) correct (1)

## Person: Robert S. Boyer

### DBLP: Boyer:Robert_S=

### Contributed to:

### Wrote 5 papers:

- PADL-2002-BoyerM #thread
- Single-Threaded Objects in ACL2 (RSB, JSM), pp. 9–27.
- CADE-1992-BoyerY #automation #correctness #proving #source code
- Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor (RSB, YY), pp. 416–430.
- CADE-1990-BoyerM #logic #proving #theorem proving
- A Theorem Prover for a Computational Logic (RSB, JSM), pp. 1–15.
- CADE-1986-BoyerM #logic #overview
- Overview of a Theorem-Prover for A Computational Logic (RSB, JSM), pp. 675–678.
- POPL-1976-BoyerMS #program transformation #recursion
- Primitive Recursive Program Transformations (RSB, JSM, RES), pp. 171–174.