Various comments:

- Solovay's comment about strength of ZFC and HOL, while true, may be misleading. I am not familiar with HOL, but I believe that it is based on the Girard-Reynolds polymorphic lambda calculus: the embedding of such a calculus into ZFC is not straightforward; see John Reynold's classic paper, `polymorphism is not set-theoretic'.
- A poster suggested thinking about translations between proof representations using category theoretic formalisms. I think this is probably a good idea. The poster also mentioned topos theory in this connection: this is possibly more work than is necessary for your purposes.
- I suggested second-order arithmetic as a good basis formalism: I think it makes life easy if most people use a single formalism, and the extra strength of ZFC is almost never necessary (also one can just add axioms to SOA to obtain equivalent strength to ZFC).