The Coq mailing list

["Carlos.SIMPSON" <Carlos.Simpson AT unice.fr>]

Dear Victor,
  Some other references which are relevant and more up-to-date are the 
works
by Jose' Grimm:
http://hal.archives-ouvertes.fr/inria-00408143/
http://hal.archives-ouvertes.fr/inria-00440786/
with the code at  http://www-sop.inria.fr/apics/gaia/


It should be pointed out that the idea of saying that my axioms 
represent some kind of `ZFC',
was maybe too hasty. The axiom schemes of ZFC have been replaced by 
statements of the
form (forall P, ...), i.e. statements quantified over propositions (or 
arrows Ens->Prop or whatever).
The exact logical status of those, in comparison with an axiom scheme in 
the classical sense
of an infinite list of explicit axioms, doesn't seem (to me) easy to 
understand.

  In order to be able to study this kind of question further, it would 
be really great if some
kind of system could be introduced to do large-scale reflection; for 
example in this particular
case we would like to be able to use the notational and unification 
facilities of coq, on the
restricted language of statements in set-theory; but then to be able to 
reflect those into
actual statements in the ground level of coq. That might also go towards 
answering
your previous question Victor:

On 11/02/2011 01:49 PM, Victor Porton wrote:
> Probably a stupid question:
>
> Why Coq has special language for writing new tactics, while Coq proofs can be 
> turn into programs? Can't programs generated from existence proof be use 
> instead of tactic scripts?
The point of this request being, that you can pretty easily define a 
language CIC or at least CC inside
Coq (see the Coq-in-Coq contribution for example); however, as far as I 
know, you can't then
use the overall big Coq program in order to handle the de Bruijn indices 
of your sub-language,
also to do the shift operation and generally unify and other things like 
that.
A large-scale reflection system would also be fantastically useful for 
interpreting
Voevodsky's homotopy type theory, back into a more standard setting.

---Carlos



On 11/03/2011 12:59 AM, Victor Porton wrote:
> Oh, I found it:
>
> http://arxiv.ccsd.cnrs.fr/e-print/math/0402336v1
>
> It is from this article:
> http://arxiv.ccsd.cnrs.fr/abs/math/0402336v1
>
> Now, admins, put these links to your wiki. I have no permission to edit the 
> page I intended to.
>
> 03.11.2011, 03:38, "Victor 
> Porton"<porton AT narod.ru>:
> > The article at http://arxiv.org/abs/math/0311260v2 about a formalization of ZF in Coq ;
> > contains "and also contains as a tar-attachment to the source file the revised and 
> > expanded version of the proof development which had been attached to 
> > math.HO/0311260".
> >
> > I have seen this .tar file earlier but now cannot find it again. Where is the 
> > tar with Coq sources?
> >
> > We need to put a reference to that tar somewhere to Cocorico in order to make 
> > its finding easier. It is an important, and as it seems to me, a well written 
> > system of modules. It should be easily findable for visitors of Coq site (now 
> > it isn't).


--


------ ------ ------ ------ ------ ------ ------ ------ ------ ------

Carlos T. Simpson
C.N.R.S., Laboratoire J. A. Dieudonne, Universite de Nice-Sophia Antipolis

"Homotopy Theory of Higher Categories" now published!

Cambridge University Press, October 2011

http://www.cambridge.org/gb/knowledge/isbn/item6172978/

------ ------ ------ ------ ------ ------ ------ ------ ------ ------