About the presentation:

Reviewer 1 is skeptical about the title: I'm not satisfied either and
would like to change it to "Program-ing Finger Trees in Coq".

Reviewers 3 and 4 complain that the contribution of the paper is in fact
twofold as it presents Russell and a certified implementation of Finger
Trees using it at the same time. I deliberately made the decision not to
focus on the theory behind Russell and its interpretation in Coq and
then present a small or sketchy Program example in part because the core
theory was already studied in an earlier work. I also preferred
presenting the main ideas behind Russell and taking the time to show how
Program really works in practice using a very detailed, substantial
example which is a contribution by itself.

Reviewer 2 suggests the original paper on Russell was not cited while it
is, at the last line of the third page, discretely for the blind review,
along with PVS.

I thank the reviewers for their diligence reporting all the errors
in phrasing and lack of clarity, precision or respect of convention.

About the content:

Reviewer 3 observes that I answer the question of termination rather
optimistically in Section 7.3. The problem is not considered in depth in
the paper but there is a demonstration of the usage of measures (in
Sections 4.4.1, 5.1) and more generally well-founded recursion (in
Section 3.2, definition of div) in addition to the usual structural
recursion criterion of Coq to ease the definition of those functions
which aren't "obviously" terminating.

Reviewers 2 and 4 complain that the scope of certification of finger
trees was not clearly defined. I state in the introduction that we prove
that every function terminates and maintains the structure invariants
which is mainly coherence of measures (which may not mean anything to
the reader at this point, hence the vagueness). Indeed append produces a
tree whose measure is equal to the concatenation of the two original
measures which ensures that no two objects were permuted by error in the
implementation. However, the exact invariant that is guaranteed by the
type of append depends entirely on the particular monoid and measure 
function used.

Finally, Program can indeed be seen as a refine on steroids: it can
accept at least the same terms with holes but has more expressiveness
due to the subtyping and the general plumbing of terms with logical
information.