The Coq mailing list

[Crist�bal Camarero Coterillo<cristobal.camarero AT alumnos.unican.es>]

I sent this to 
coqdev AT inria.fr
 and I was told that better to send to this list.
Maybe it is of interest to someone.

>
> People of the Coq system,
>
> First, I apologize if I am addressing to the wrong people and for consuming
your
> time. I am a student in the University of Cantabria on the degree of 
> computer
> science (Ingienería Informática).
>
> I discovered Coq nearly two months ago and I've been playing with it since
then
> in my free time; it is probably the most beautiful thing I have ever seen.
> I have uploaded some of the things I made in my page at
> http://www.alumnos.unican.es/ccc66/coq.htm
> Maybe you like some of them.
> I were aiming to prove in Coq a result of myself, accepted for the IWONT2010
> dealing with automorphism of Cayley graphs over Abelian groups, so I built
> the necessary background and begin to prove things. Unfortunately the last
> theorem I was aspiring to prove evades my grasp because I use to prove it
> (in paper) a summatory (with sum being the group operation). I proved some
> lemmas of reductions (folds) of a set but it gets complicated.
>
> I would really like to know your opinion.
>


--Cristóbal Camarero Coterillo

Universidad de Cantabria
http://www.alumnos.unican.es/ccc66
cristobal.camarero AT alumnos.unican.es
nakacristo AT hotmail.com