Is it possible to express Coq Calculus of Constructions in terms of Isabelle/HOL or vice versa? If that could be done then we would be able to import Coq axioms and theorems in Isabelle/HOL. Coq has great formalisation of analysis and differential equations and Isabelle/HOL environment could greatly benefit from this corpus of formalized math.
There is project http://dedukti.gforge.inria.fr/ that expresses both Coq and Isabelle/HOL in new type theory (but not among themselves). Maybe that is the right path ahead.
There is a fair amount of research in this area already. See e.g. the work by Chantal Keller; her paper with Benjamin Werner (https://hal.inria.fr/file/index/docid/520604/filename/itp10.pdf) describes a translation from HOL Light to Coq.