On behalf of the program committee of the 20000 workshop on Implicit Computational Complexity I am pleased to inform you that your paper,

Your paper has been read by several of the program committee members. Below please find portions of the reports which may be of value to you in preparing your results for presentation at the workshop or in a final journal article.

I will put on-line the accepted submissions, on the web pages of ICC'00. Contributed papers will each be presented in a 25 minute talk at the workshop, either on June 29, or 30. The workshop program will be finalized and made public in the near future.

You have to register. Since we were late on the referee process, S. Vito (svito@housing.ucsb.edu) kindly accept that you pay early registration fee.

- I think that you have to say that you are a ICC speaker -

Thank you for submitting a paper to the ICC'00 workshop. I am looking forward to seeing you in Santa-Barbara for the meeting.

With best wishes

Jean-Yves Marion, ICC'00 chair

================================================
Referee report on Klaus Aehlig's ICC submission.

This paper describes an arithmetic corresponding to Hofmann's system
for non-size increasing polynomial time computation presented at
LICS99. Proofs in this arithmetic can be translated in such a way that
a proof of a Pi02 statement of a certain form gives rise to a Skolem
function in Hofmann's system.

Essentially the same functionality is provided by a logic developed by
Berger, Hofmann, and Schwichtenberg (unpublished draft cited in
Schwichtenberg-Aehlig's LICS'00 paper, hence known to Aehlig). In the
referee's opinion the Berger et al system is more elegant than the one
in the paper under review because it uses a more economical syntax and
fewer rules. However, the topic is important enough to allow for
alternative approaches and therefore I recommend acceptance on
condition that the version to be presented at the workshop contains a
reasonably detailed comparison with Berger, Hofmann, Schwichtenberg's
system.

The technical development in the paper under review appears to be
sound. The following are minor comments mainly of aesthetical nature.

p1, abstract: It is not necessarily the case that a function with a
proof of n
nested inductions is O(x^n) computable. Rather is O(x^n) a bound on
the number of reduction steps as well as on the size of intermediate
terms. Since a reduction step takes time linear in the size of the
involved terms we have time complexity O(x^{2n}). Probably this can be
shrunk by a further analysis, but no such analysis is provided.

p3: The following comment also applies to the LICS00 paper by Aehlig
and Schwichtenberg: In the beta rule (lambda x.t)s -> t[s/x] it may be
the case that x occurs twice in t, namely in a  expression. If
we simply perform the beta reduction then we may double the size hence
get exponentially intermediate terms in an iteration. One must delay
such beta reductions until the pair  is resolved.

p3 Formulae. The existential quantifier should really be called
$\exists$ and not $\exists^*$ because like $\forall$ and unlike
$\forall^*$ it has computational content.

p3 Proof terms. In my opinion the proof terms are unnecessary
clutter. It would suffice to present the proof system in the usual way
using rules and to show by rule induction that every proof has a
realiser. Obviously, in an implementation a formal representation of
proofs would be needed, but this is a trivial engineering problem and
does not belong into the paper. It would of course be a different
matter if the proof terms were manipulated in one way or the other
(e.g. normalised, formally checked, etc) but this is not the case.