@@ -3,13 +3,19 @@ Our translation covers entirely the syntax of the Coq language and it preserves

Moreover, we are confident that, if and when future work yields a complete formalization of the Coq typing rules in an LF-like logical framework, our translation will be in a format suitable for rechecking the entire library --- with the obvious caveat that such a rechecking would face even more serious scalability issues than we had to overcome so far.

\CSC{An obvious way to verify that the exported information is sound and complete for type-checking would be to implement an importer for Coq itself or, in alternative, for an independent verifier for the logic of Coq, like the one implemented in Dedukti or the one developed in the HELM/MoWGLI projects~\cite{DBLP:journals/amai/AspertiPCGS03} and later incorporated into Matita 0.5.x series~\cite{DBLP:conf/cade/AspertiRCT11}. In both cases one would need to develop a translation from MMT theories to the modular constructs of the language, which requires more research. For example, no translation of MMT theories and theory morphisms into modules, module types and functors is currently known.}

\CSC{We would also like to stress that independent verification is not the aim of our effort: the main point of exporting the library of Coq to MMT is to allow independent services over them, like queries, discovery of alignments with libraries of other tools or training machine learning advisers that can drive hammers. Most of these services can be implemented even if the typing information is incomplete or even unsound (e.g. if all unvierses are squashed to a single universe, making the logic inconsistent).}

\paragraph{Limitations and Future Work}

Our translation starts with the Coq kernel data structures and is thus inherently limited to the structure seen by the kernel.

Therefore, record types and type classes are presented just as inductive types, that is the way they are elaborated before passing them to the kernel.

This is unfortunate as recent Coq developments, most importantly the Mathematical Components project \cite{gonthier_packaging}, have made heavy use of records to represent theory graph--like structuring and an unelaborated representation would be more informative to the user and to reasoning tools.

In fact, even sections are not visible to the kernel, and we were able to include them because we were able to reconstruct the section structure during our translation.

We expect that similar efforts may allow for including record types and canonical structures in the theory graph in the future.

We expect that similar efforts may allow for including record types and canonical structures in the theory graph in the future \CSC{and we plan to start working on that next.}

\CSC{Many libraries avoid module and functors and achieve modularity using other more recent features of Coq that are invisible at the kernel level, like type classes. Moreover type classes, canonical structures, coercions, etc. are necessary information to extend a library because they explain how the various mathematical notions are meant to be used. While the already cited services that we plan to provide do not depend on them, importing the library in another system to build on top of it surely does. Therefore a future challenge will be to find system independent generalizations and representations of such constructs, which will be necessary to incorporate them into a logic and system independent tool like MMT.}

Our formal representation of the Coq logic is untyped, i.e., we use a single type in the logical framework for all Coq expressions.

As we explain in Sect.~\ref{sec:logic}, we consider a typed representation infeasible at this point.