Refereed Papers

• Regulating CCTV.
  Proceedings of Ethicomp 2007 (Vol 1).
  Meiji University, 2007; ISBN: 4-9903558-0-7; pp. 3-14

• Perspex Machine VIII: Axioms of Transreal Arithmetic.
  Vision Geometry XV, Proceedings of the SPIE-IS&T Electronic Imaging.
  SPIE Vol. 6499, 2007; ISBN 0-819-46612-9
  Joint work with Anderson and Völker.

• Valid Protection or Abusive Control? DRM, Law and Technology.
  International Review of Law, Computers and Technology; Volume 20(3), 2006; ISSN: 1360-0869/1364-6885; pp. 233-237.

• Customer-Driven Development for Rapid Production of Assessment Learning Objects.
  Electronic Journal of e-Learning; Volume 4(1), 2006; ISSN 1479-4403; pp. 1-6.
  Joint work with Williams.

• The Effectiveness of Assessment Learning Objects Produced Using Pair Programming.
  Electronic Journal of e-Learning; Volume 2(2), 2004; ISSN 1479-4403; pp. 247-256.
  Joint work with Lubega, Walmsley and Williams.

• Digitisation, Representation and Formalisation: Digital Libraries of Mathematics.
  Mathematical Knowledge Management.
  Springer ``LNCS 2594'', 2003; ISBN: 3-540-00568-4; pp. 1-16.

• Definite Integration of Parametric Rational Functions.
  Symbolic Computation and Automated Reasoning.
  A. K. Peters, 2001; ISBN:1-56881-145-4; pp. 3-17.

• Computer Algebra meets Automated Theorem Proving: Integrating Maple and PVS.
  Theorem Proving in Higher Order Logics.
  Springer ``LNCS 2152'', 2001; ISBN: 3-540-42525-X; pp. 27-42.
  Joint work with Dunstan, Gottliebsen, Kelsey, Martin and Owre.

• A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs.
  LMS Journal of Computation and Mathematics; Volume 3, 2000; ISSN: 1461-1570; pp. 1-26.

• Automated theorem proving in support of computer algebra: symbolic definite integration as a case study.
  Proceedings of the 1999 International Symposium on Symbolic and Algebraic Computation.
  ACM Press, 1999; ISBN: 1-58113-073-2; pp. 253-260.
  Joint work with Gottliebsen, Linton and Martin.

• VSDITLU: a verifiable symbolic definite integral table look-up.
  Automated Deduction -- CADE16.
  Springer ``LNAI 1632'', 1999; ISBN: 3-540-66222-7; pp. 112-126.
  Joint work with Gottliebsen, Linton and Martin.