Commit 9aa5589e authored by Florian Rabe's avatar Florian Rabe

no message

parent e4d7f6a5
......@@ -17,9 +17,8 @@ We expect that similar efforts may allow for including record types and canonica
\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.
Moreover, our representation does not include the typing rules.
This is not due to a principal limitation: it is possible to add these rulesto let \mmt type-check the library.
But formalizing the Coq type system is in itself a major challenge, and representing the details of, e.g., Coq's treatment of pattern matching or sort polymorphism may even require innovations in logical framework design.\ednote{DM: Talk about applications}
Our formal representation of Coq declarations includes the types of all constants and variables, but 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 of expressions infeasible at this point.
Our representation does not include the typing rules for the expression, but this is not due to a principal limitation: it is possible to add these rules to let \mmt type-check the library.
But formalizing the rules of the Coq type system is in itself a major challenge, and representing the details of, e.g., Coq's treatment of pattern matching or sort polymorphism may even require innovations in logical framework design.\ednote{DM: Talk about applications}
......@@ -36,14 +36,13 @@ Mizar in \cite{IKRU:mizar:11}, HOL Light in \cite{KR:hollight:14}, PVS in \cite{
This overall line of research was presented in \cite{KR:qed:14}.
Similarly, to the \mmt research, proof assistant libraries have been exported into Dedukti \cite{dedukti}.
While \mmt exports focus on preserving the original structure, Dedukti exports focus on reverifying proofs.
Coqine is the tool used for translating Coq to Dedukti.\ednote{@FR: rewrite this}
Coqine is the tool used for translating Coq to Dedukti, and while \mmt exports focus on preserving the original structure, Coqine focuses on reverifying proofs.
Unlike our logic definition, Coqine includes a formalization of the typing rules in order to type check the export.
However, this translation eliminates some features of the Coq logic in order to simplify the typing rules and, contrary to our export, does not handle the full Coq library.
The original version \cite{coqine} covered most of the small standard library.
But it used severe simplifications like collapsing the universe hierarchy.
In order to make this feasible, this translation eliminates several features of the Coq logic so that the typing rules become simpler.
Our export, on the contrary, makes the dual trade-off, covering the entire logic at the expense of representing the typing rules.
Concretely, the original version \cite{coqine} covered most of the small standard library, using simplifications like collapsing the universe hierarchy.
A later reimplementation \cite{assafphd} used a more faithful representation of the logic.
But it omitted several language features such as modules, functors and universe polymorphism and therefore could not translate a significant part of the library.
But it still omitted several language features such as modules, functors and universe polymorphism and therefore could not translate a significant part of the library.
\cite{coqhammer} develops a translation of Coq into first-order logic in order to apply automated provers as hammers.
Like Coqine, it only covers a subset of the language.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment