Experience with Embedding Hardware Description Languages in HOL. - Richard J. Boulton; Andrew D. Gordon 001; Michael J. C. Gordon; John Harrison 001; John Herbert; John Van Tassel (TPCD, 1992)

A Lazy Approach to Fully-Expansive Theorem Proving. - Richard J. Boulton (TPHOLs, 1992)

Boyer-Moore Automation for the HOL System. - Richard J. Boulton (TPHOLs, 1992)

Lazy Techniques for Fully Expansive Theorem Proving. - Richard J. Boulton (Formal Methods Syst. Des., 1993)

Efficiency in a fully-expansive theorem prover. - Richard J. Boulton (1993)

A Restricted Form on Higher-Order Rewriting Applied to an HDL Semantics. - Richard J. Boulton (RTA, 1995)

Combining Decision Procedures in the HOL System. - Richard J. Boulton (TPHOLs, 1995)

A Tool to Support Formal Reasoning about Computer Languages. - Richard J. Boulton (TACAS, 1997)

System Description: An Interface Between CLAM and HOL. - Konrad Slind; Michael J. C. Gordon; Richard J. Boulton; Alan Bundy (CADE, 1998)

Iterative Dialogue and Automated Proofs. - Konrad Slind; Richard J. Boulton (FroCoS, 1998)

Generating Embeddings from Denotational Descriptions. - Richard J. Boulton (TPHOLs, 1998)

An Interface between Clam and HOL. - Richard J. Boulton; Konrad Slind; Alan Bundy; Michael J. C. Gordon (TPHOLs, 1998)

System Description: CyNTHIA. - Jon Whittle 001; Alan Bundy; Richard J. Boulton; Helen Lowe (CADE, 1999)

An ML Editor Based on Proofs-As-Programs. - Jon Whittle 001; Alan Bundy; Richard J. Boulton; Helen Lowe (ASE, 1999)

Transparent Optimisation of Rewriting Combinators. - Richard J. Boulton (J. Funct. Program., 1999)

Towards Automating Inductive Proofs for State Monads. - Richard J. Boulton (ARW, 2000)

Automatic Derivation and Application of Induction Schemes for Mutually Recursive Functions. - Richard J. Boulton; Konrad Slind (Computational Logic, 2000)

The PROSPER Toolkit. - Louise A. Dennis; Graham Collins; Michael Norrish; Richard J. Boulton; Konrad Slind; Graham Robinson; Michael J. C. Gordon; Thomas F. Melham (TACAS, 2000)

Object Muscat, an Open search engine. - Martin Porter; Richard J. Boulton (SIGIR Forum, 2000)

Proofs-as-Programs as a Framework for the Design of an Analogy-Based ML Editor. - Jon Whittle 001; Alan Bundy; Richard J. Boulton (Formal Aspects Comput., 2002)

A Hoare Logic for Single-Input Single-Output Continuous-Time Control Systems. - Richard J. Boulton; Ruth Hardy; Ursula Martin (HSCC, 2003)

The PROSPER toolkit. - Louise A. Dennis; Graham Collins; Michael Norrish; Richard J. Boulton; Konrad Slind; Thomas F. Melham (Int. J. Softw. Tools Technol. Transf., 2003)

Design Verification for Control Engineering. - Richard J. Boulton; Hanne Gottliebsen; Ruth Hardy; Tom W. Kelsey; Ursula Martin (IFM, 2004)

Computer Assisted Reasoning. - Richard J. Boulton; Joe Hurd; Konrad Slind (J. Autom. Reason., 2009)