| 2005 | AAAI | Proving Theorems of Type Theory Automatically with TPS. | Peter B. Andrews |
| 2000 | CADE | Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic. | Peter B. Andrews, Chad E. Brown |
| 2000 | CADE | System Description: TPS: A Theorem Proving System for Type Theory. | Peter B. Andrews, Matthew Bishop, Chad E. Brown |
| 1998 | CADE | Selectively Instantiating Definitions. | Matthew Bishop, Peter B. Andrews |
| 1996 | TABLEAUX | On Sets, Types, Fixed Points, and Checkerboards. | Peter B. Andrews, Matthew Bishop |
| 1990 | CADE | The TPS Theorem Proving System. | Peter B. Andrews, Sunil Issar, Dan Nesmith, Frank Pfenning |
| 1988 | CADE | The TPS Theorem Proving System. | Peter B. Andrews, Sunil Issar, Daniel Nesmith, Frank Pfenning |
| 1986 | CADE | Connections and Higher-Order Logic. | Peter B. Andrews |
| 1986 | CADE | The TPS Theorem Proving System. | Peter B. Andrews, Frank Pfenning, Sunil Issar, Carl P. Klapper |
| 1982 | CADE | A Look at TPS. | Dale A. Miller, Eve Longini Cohen, Peter B. Andrews |
| 1980 | CADE | Transforming Matings into Natural Deduction Proofs. | Peter B. Andrews |
| 1977 | IJCAI | Theorem Proving in Type Theory. | Peter B. Andrews, Eve Longini Cohen |