Taking you at your word I offer the following observations on your abstract:
<snip>
> The plan of the paper is as follows. We examine ways of providing user
> extensibility for theorem provers, which naturally places the LCF and
> reflective approaches in opposition.
I don't see why a reflection principle should be regarded as "in opposition"
to the LCF paradigm. The LCF paradigm can be applied to any logic however
complex its rules. A reflection principle can be put into a logic and
implemented as a rule, using the LCF paradigm, in complete consistency with
anything that I would regard as essential to that paradigm.
I'm not suggesting that your primary concern isn't a real one, which is
about whether doing this would be worthwhile. Just quibbling with your
description of the issue.
I would be interested to hear what the qed community considers to be
the definitive characteristic(s) of the LCF paradigm.
Roger Jones http://www.to.icl.fi/ICLE/rbjpub/rbj.htm
at home rbj@campion.demon.co.uk