We thank the reviewers for their detailed and insightful reviews.
All reviewers had comments about poor readability due to the technical nature and of
lacking motivation/application. In particular:
a. Reviewers 3/4/5 want to know about services/improvements to the ITP and MKM
communities. We believe it is desirable to build a framework in which all languages
(ITP/CAS/MKM) can be naturally represented. Our experience (especially in the OAF project,
where we import ITP libraries: Mizar, HOL Light, Coq, PVS, etc.) has shown that a mechanism
like the one proposed is indispensable to bring order into the zoo of language
features. This was clear to us, but must be clarified in the introduction.
b. Reviewer 1 asks about the rationale behind the specific extensions and related work: Many
ITP/MKM systems have ad-hoc elaboration-based language features, that differ between
systems. Our contribution is a uniform mechanism that subsumes them and can serve for
systematic modelling of such features and as a basis for establishing interoperability
between ITP/MKM languages.
We believe that we can remedy motivation and readability of the technical contribution by
improving the introduction (in terms of a) and b)), moving examples forward, and
systematically moving technical details to a separate section at the end so that the main
contribution of the paper becomes self-contained. This will also give us a chance for
further clarification of the syntax.
Particulars:
Reviewer 1 asks about completeness of the characterization: The proposed design and
features are evaluated with respect to the OAF examples. For these the design is adequate
and the main declaration-level language features are all covered. We acknowledge and will
discuss in the paper that there is a trade-off between completeness, modelling accuracy,
and tractability of the framework.
Motivation:
Reviewer 1 asks about "not every feature can be defined in all detail" this is caused by
the page limit, not the framework; we will clarify this in the paper.
One common issue was the insufficient discussion motivating our design choice and
its benefits for the community: Reviewer 1 asks about the rationale behind the
specific extensions and related work while Reviewers 3/4/5 inquire about
services/improvements to the ITP/MKM communities.
Reviewer 3: we will update the web page.
We believe it is desirable to build a framework in which all ITP/CAS/MKM languages
can be naturally and uniformly represented. Many ITP/MKM systems have various elaboration-based language features, but they are ad-hoc and differ between systems
Our experience (especially in the OAF project, where we import ITP libraries: Mizar, HOL Light, PVS, Coq, etc.)
has shown that a framework like we propose is indispensable to bring order into the zoo of language features.
The design and implementation of structural features as a mechanism for systematically modeling and studying such language features is motivated by this experience.
It also allows reusing our existing generic applications and services
(eg. IDE, search, change management, type checking). We will clarify this in the introduction.
Readability:
Another common issue was the readability and self-containedness of the paper.
Currently, we describe the intricacies of the formalism before giving sufficient motivation and concrete examples.
We believe we can remedy this by improving the introduction and motivation along the lines described above,
moving the examples section forward, and systematically moving technical details (inference system) to a separate section at the end.
Therefore, the main contribution of the paper becomes self-contained. This will also let us further clarify the syntax.
Reviewer 5 mentions ambiguity between the "definition 1" in the example and the first
definition of the paper. Of course we will fix this.
Other Issues:
Reviewer 6 is concerned about locality and compositionally.
Reviewer 6 is concerned about locality and compositionality.
Elaboration reduces the semantics of each structural feature to that of MMT. Thus, all
categorical constructions of the category of MMT theories remain possible.
However, it is desirable to have a notion of theory morphism that allows working with
structural features directly (i.e., without elaborating them). We wrote a section
structural features directly (without elaborating them). We wrote a section
that provides sufficient conditions for that but removed it because it made the paper too
long and too technical. We will add a brief discussion of that in the final version.
long and too technical. We will add a brief discussion of that.
Reviewer 1 asks about completeness of the characterization.
The proposed design and features are evaluated with respect to the OAF libraries: For these the design is adequate
and the main declaration-level language features are all covered. However, there is a trade-off between completeness,
modeling accuracy, and tractability of the framework. We will discuss this in the paper.
Reviewer 1 asks about "not every feature can be defined in all detail" this is caused by
the page limit, not the framework; we will clarify this.
Reviewer 3: we will update the web page.
Reviewer 5 mentions ambiguity between the definition numbering in the example and the paper.
We will fix this alongside all other minor comments the reviewers had.
