This paper is part of a project to link the HOL4 and ACL2 systems. Warren Hunt and I started writing it during Warren's summer visit to Cambridge in 2005. It was revised following detailed comments from Matt Kaufmann and others. During and after Matt's later visit to Cambridge, the ideas were refined and the implemention started by Mike and Warren revised and extended.

• Version 1.5 is obsolete and mainly describes the work done by Mike and Warren, but it incorporates some comments from Matt.

• Version 2.4 [ tex | pdf | postscript] of the paper reflects our current thinking and describes changes made to our methodology and tools following Matt's visit.

The main developments from Version 1.5 to Version 2.4 are:

1. Numbers are modelled correctly by complex rationals. The HOL type complex_rational is defined using a rational number package due to Jens Brandt of University of Kaiserslautern.

2. The exact ACL2 names of functions and constants are used in HOL. Since these names may violate the lexographic rules of the HOL parser, each ACL2 function is given a HOL friendly name.

3. All the 31 ACL2 primitives have been defined in HOL. Thus the HOL SEXP layer is now complete and fully implements all of the ACL2 logic.

4. Matt has implemented in ACL2 some tools for moving definitions, theorems and axioms between HOL and ACL2.

5. There are two appendices.
   1. Appendix 1 partially documents the tools implemented so far;
   2. Appendix 2 lists the HOL definitions of the ACL2 primitives.