\mmt provides the semantics that ties together the three involved levels (logical framework, logic, and library) and provides a uniform high-level API for further processing.
\cite{KohRab:eempal20} gives on overview over the theoretical, technical, and social challenges of the OAF exports.
\begin{newpart}{FR: Reviewer 2's comment on reusing export techniques}
In the work reported here, we follow this basic recipe with a few modifications.
Firstly, because Isabelle already includes a logical framework, we do not encode Isabelle in yet another one.
Instead, we extend the existing LF formalization in \mmt to obtain one for the Pure framework of Isabelle.
...
...
@@ -63,7 +62,6 @@ There are two reasons for this choice: it is conceptually appropriate as it puts
Secondly, Isabelle is extremely complex, and a large portion of our work went to streamlining Isabelle components to enable step (ii) above.
Thirdly, the resulting exports of the Isabelle libraries were significantly larger than any exports we had handled previously.
Therefore, we had to develop new optimizations both on the Isabelle and on the \mmt side to be able to carry out step (iii) above.
\end{newpart}
%It is critical that the exports systematically avoid any (deep) encoding of logical features.
%That is important so that further processing can work with the exact same structure apparent to a user of the proof assistant. \ednote{Talk about the the rest of the OMDoc/MMT import/export business}
...
...
@@ -78,10 +76,8 @@ We present preliminaries about Isabelle and PIDE as well as \omdoc and \mmt in S
Then we describe the logical and the technical aspects of the export in Sections~\ref{sec:logical} and~\ref{sec:technical}.
We sketch some applications enabled by the export in Section~\ref{sec:applications}.
\begin{newpart}{Reviewer 1's comment on division of work; @Michael: check this}
It is difficult to estimate the total workload covered by this paper because it builds on decades of implementation work in both Isabelle and \mmt, much of which was never published in itself.
But concretely for this particular export, we spent about 1 person-month on the overall design of the translation and the implementation, 6 person-months on the implementation on the Isabelle side, 1 on the \mmt side, and 1 on administrative parts and dissemination of the results.
\end{newpart}
\subparagraph{Acknowledgments}
The authors were supported by DFG grant RA-18723-1 OAF and EU grant Horizon 2020 ERI 676541 OpenDreamKit.
@@ -87,11 +87,17 @@ The possible morphisms in \mmt are \textbf{inclusions}, which import all declara
Figure~\ref{fig:tgraph} shows an example of a typical setup of formalizations in \mmt: Dotted lines represent the meta-theory-relation, hooked arrows are includes, squiggly arrows represent views, and the normal arrows represent named structures.
Here LF is used as a logical framework to define some logics, which are then used as meta-theories for algebraic theories.
<<<<<<< HEAD
\begin{newpart}{MK: an extension which explains the setup}
We see three pragmatic levels: the logical frameworks at the top, logics in the middle, and the domain theories at the bottom.
Meaning trickles down from the theories at the top (the ones without meta-theories), which are implemented directly in \mmt/Scala as described for LF above.
This setup can even encode model theory theory morphisms into semantic theories like ZFC set theory.
\end{newpart}
=======
We see three pragmatic levels: the logical frameworks (meta-meta-theories) at the top, logics (meta-theories) in the middle and the domain theories at the bottom.
Meaning trickles down from \emph{ur-theories} -- which have no meta-theory and which are implemented directly in MMT/Scala as described for LF above -- via the meta-theory-relation.
This setup can even encode model-theory via views (interpretations) into foundational theories like ZFC set theory.
