| Computer Assisted Reasoning | 0 | 0.34 | 2009 |
| The PROSPER toolkit | 4 | 0.65 | 2003 |
| A Hoare logic for single-input single-output continuous-time control systems | 14 | 0.92 | 2003 |
| Proofs-as-Programs as a Framework for the Design of an Analogy-Based ML Editor | 1 | 0.36 | 2002 |
| Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings | 22 | 2.89 | 2001 |
| The PROSPER Toolkit | 43 | 2.38 | 2000 |
| Automatic Derivation and Application of Induction Schemes for Mutually Recursive Functions | 8 | 0.55 | 2000 |
| Transparent optimisation of rewriting combinators | 1 | 0.38 | 1999 |
| Generating Embeddings from Denotational Descriptions | 3 | 0.45 | 1998 |
| System Description: An Interface Between CLAM and HOL | 8 | 0.58 | 1998 |
| An Interface between Clam and HOL | 27 | 2.63 | 1998 |
| A Tool to Support Formal Reasoning about Computer Languages | 4 | 0.48 | 1997 |
| A Restricted Form on Higher-Order Rewriting Applied to an HDL Semantics | 2 | 0.42 | 1995 |
| Combining Decision Procedures in the HOL System | 6 | 0.88 | 1995 |
| Lazy Techniques for Fully Expansive Theorem Proving | 8 | 0.82 | 1993 |
| Experience with Embedding Hardware Description Languages in HOL | 95 | 7.33 | 1992 |
| Boyer-Moore Automation for the HOL System | 5 | 0.53 | 1992 |
| A Lazy Approach to Fully-Expansive Theorem Proving | 4 | 1.04 | 1992 |
