The Coq mailing list

[casteran AT labri.fr]

Quoting "Jorge F. Salas O." 
<jfsalaso AT cantv.net>:

> Dear Sir,
>
> We, at the Escuela de Computación de la Universidad Central de   
> Venezuela, are beginning to use Coq as a tool for realize proofs and  
>  extract functional programs from them. We are interested in using   
> Coq especifically for proving theorems in the theory of formal   
> languages, mainly in linear and context-free languages. By example,   
> the equivalence between finite automata and linear languagues, the   
> pumping lemma, etc.
>
> We are using Bertot & Castéran book for learning the system and in   
> september we will conduct a seminar in the Calculus of Constructions  
>  and the Curry-Howard isomorphism.
>
> I ask you advice in order to find previous and recent results in this
> class of problems using Coq. Best if we can get a tutorial in using Coq
> for proving theorems in the formal language theory.
>
> Thanking you in advance.

 Dear Prof. Salas,

There are interesting contributions on formal language theory:
http://coq.inria.fr/contribs-eng.html

Please look also at the section on Concurrent Systems and Protocols.

The authors of these contributions certainly would tell you how to get
reports on these developments.

Best regards,

Pierre



> --
> Prof. Jorge F. Salas O.
> Laboratorio Mefis
> Escuela de Computación
> Facultad de Ciencias - UCV
> Tel. 605.1042/1070

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.