Integrating Gandalf and HOL. - Joe Hurd (TPHOLs, 1999)

Predicate Subtyping with Predicate Sets. - Joe Hurd (TPHOLs, 2001)

Congruence Classes with Logic Variables. - Joe Hurd (Log. J. IGPL, 2001)

An LCF-Style Interface between HOL and First-Order Logic. - Joe Hurd (CADE, 2002)

A Formal Approach to Probabilistic Termination. - Joe Hurd (TPHOLs, 2002)

Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem Proving. - Michael J. C. Gordon; Joe Hurd; Konrad Slind (CHARME, 2003)

Applications of Polytypism in Theorem Proving. - Konrad Slind; Joe Hurd (TPHOLs, 2003)

Verification of the Miller-Rabin probabilistic primality test. - Joe Hurd (J. Log. Algebraic Methods Program., 2003)

Functional Correctness Proofs of Encryption Algorithms. - Jianjun Duan; Joe Hurd; Guodong Li; Scott Owens; Konrad Slind; Junxing Zhang (LPAR, 2005)

Probabilistic guarded commands mechanized in HOL. - Joe Hurd; Annabelle McIver; Carroll Morgan (Theor. Comput. Sci., 2005)

Proof Pearl: The Termination Analysis of Terminator. - Joe Hurd (TPHOLs, 2007)

Data Assurance in Opaque Computations. - Joe Hurd; Guy Haworth (ACG, 2009)

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

Composable Packages for Higher Order Logic Theories. - Joe Hurd (VERIFY@IJCAR, 2010)

Evaluation Opportunities in Mechanized Theories. - Joe Hurd (EMSQMS@IJCAR, 2010)

The OpenTheory Standard Theory Library. - Joe Hurd (NASA Formal Methods, 2011)

Standalone Tactics Using OpenTheory. - Ramana Kumar; Joe Hurd (ITP, 2012)

Using Term Rewriting to Solve Bit-Vector Arithmetic Problems - (Poster Presentation). - Iago Abal; Alcino Cunha; Joe Hurd; Jorge Sousa Pinto (SAT, 2012)