The official specification of ACL2 can be found in the papers A Precise Description of the ACL2 Logic and Structured Theory Development for a Mechanized Logic.
ACL2 has a number of features that make it highly suitable for system modelling. Our goal is to enable HOL users to employ ACL2 as a trusted oracle. A specific case study we have in mind is to experiment with ACL2 for executing the verified ARM model due to Anthony Fox.
ACL2PII is our starting point. However, the Prosper Toolkit, though influential and successful in its time, is no longer supported and HOL methodology has moved on. In particular, Konrad Slind has been developing a polytypism methodology for systematically processing and translating higher order logic terms. One (of several) applications is the translation from higher order logic to ML programs, so that ML can be used as an execution oracle for ground HOL terms.
One of the tricky things about translating from the untyped ACL2 logic to typed higher order logic is figuring out which types to assign. An example Staples gives is that, depending on the context, the ACL2 S-expression NIL might need to be translated to F (falsity of HOL type bool), or [] (the empty list) or NONE (the empty option). The ACL2PII user has to set up "translation specifications" that are pattern-matching rewrite rules to perform the ACL2 to HOL translation. These are encoded in ML and are thus outside the fully-expansive LCF methodology (and so may introduce inconsistency).
Inspired by Konrad's polytypism methodology, it is hoped to use a deeper linking, with families of semantic functions defined in higher order logic to perform the coding/decoding bewtween higher order logic and the ACL2 S-expressions. These Slind-style translation functions will be based on a semantics of the ACL2 logic in HOL (deep embedding) and should enable some formal assurance that the translations between the logics is sound. In Appendix A of Linking ACL2 and HOL, Staples gives the following definition of ACL2 S-expressions in HOL:
type_abbrev("packagename", ``:string``);
type_abbrev("name", ``:string``);
Hol_datatype
`sexp = ACL2_SYMBOL of packagename => name
| ACL2_STRING of string
| ACL2_CHARACTER of char
| ACL2_NUMBER of num
| ACL2_PAIR of sexp => sexp`;
Define `ACL2_NIL = ACL2_SYMBOL "ACL2" "NIL"`
Define `ACL2_T = ACL2_SYMBOL "ACL2" "T"`
There is one piece of background that may (but probably won't) turn out to be useful. This is the (somewhat unsuccessful) attempt to translate between untyped ZF set theory and higher order logic. The approach used was, like Staples', quite "shallow" (i.e. performed by metalanguage scripts rather than by proof). This endeavour floundered because the logical foundation of the translation scripts wandered into parts of set theory where I was out of my depth. I came away from the exercise feeling that it needed to be done more inside higher order logic, so as to ensure the various logical transformations were formally validated by HOL. This colours my reading of Staples' more successful ACL2PII work, and is one reason why I want to try a "deeper" approach to embedding.
Several people have looked into linking classical and constructive higher order logics. For example, Encoding the HOL Light logic in Coq - Freek Wiedijk, Importing Isabelle Formal Mathematics into NuPRL - Naumov (1999) and Semantic foundations for embedding HOL in Nuprl - Howe - 1996. These and similar papers tend to have scary math, but there might be some insights lurking in them.