Proposition pour la prochaine séance : l'assistant de preuves formelles Coq

[Maxime Folschette]

Bonjour à tous,

Pour la prochaine séance du Nantes FP Group et après discussion avec Clément, je vous propose une séance autour de Coq [1], qui est un assistant de preuves formelles.
Certains se demanderont peut-être à première vue quel rapport cela pourra avoir avec la programmation fonctionnelle, mais le lien est en réalité très étroit.

En quelques mots, Coq permet de définir des objets mathématiques à l'aide du langage Gallina (qui est purement fonctionnel). Ces objets peuvent globalement prendre la forme de types, fonctions ou propositions mathématiques. Dans un deuxième temps, Coq permet, à l'aide d'un environnement de démonstration bien fourni, d'effectuer la preuve des diverses propositions que vous avez avancées.
Un exemple très simple (et très courant) d'utilisation de Coq, qui sera certainement le premier exemple de la séance, est la définition de l'ensemble des entiers naturels, puis la définition de l'addition sur ces entiers. Par la suite, on pourra vouloir prouver sont la commutativité et l'associativité de cette opération.
L'utilisation de Coq peut aller très loin. On peut notamment s'en servir pour prouver des programmes impératifs à l'aide de logique de Hoare par exemple [2]. Il a aussi permis la démonstration de certains théorèmes, donc le plus célèbre est le théorème des quatre couleurs [3].

Son lien étroit avec la programmation fonctionnelle, outre le langage Gallina, se situe au niveau d'une notion qu'on appelle l'isomorphisme de Curry-Howard, qui stipule la présence d'une correspondance entre preuve et fonction mathématique. Cette correspondance est un peu subtile, mais je vous propose de la découvrir au terme de cette séance, ou d'une seconde séance si nécessaire.

Je vous propose donc le programme suivant (assez conséquent) autour de Coq :
1) Introduction à Coq et au langage de description Gallina : définitions basiques d'objets mathématiques et utilisation de l'environnement de preuves ;
2a) Preuve de programmes impératifs : après avoir défini la grammaire et la sémantique d'un langage impératif simple, il devient possible de prouver que celui-ci observe le comportement désiré ;
2b) Présentation de l'isomorphisme de Curry-Howard : il est possible de se passer de l'environnement de preuves de Coq et d'écrire les preuves de théorèmes sous forme de fonctions, leur correction étant assurée grâce au typage fort de Gallina.

Ce programme se divise en deux branches (2a et 2b) qui ne sont pas antinomiques, mais qui auraient plutôt intérêt à être traitées séparément. Je souhaiterais ainsi avoir un retour de votre part afin de savoir :
— d'une part si ce sujet vous intéresse,
— d'autre part quel aspect (parmi 2a et 2b) vous préféreriez étudier (« les deux » étant une réponse tout à fait acceptable).

Il restera aussi à discuter de la charge d'une telle séance (il sera possible de la diviser si le sujet semble trop complexe pour être traité en une fois), et naturellement de la date.

Ceux qui sont curieux à propos de Coq pourront consulter un tutoriel [2] et un livre [4] à son propos.

En attendant votre réponse je vous souhaite une bonne fin de semaine,

Maxime


[1] http://coq.inria.fr/
[2] http://www.cis.upenn.edu/~bcpierce/sf/
[3] https://fr.wikipedia.org/wiki/Th%C3%A9or%C3%A8me_des_quatre_couleurs
[4] http://www.labri.fr/perso/casteran/CoqArt/index.html

[Pierre-Alexandre Voye]

Moi ça me tente parce que ça fait 10 ans que je tourne autour sans jamais m'y mettre sérieusement.
C'est passionnant et c'est important de sensibiliser les gens à ça.
Après je pense qu'il va falloir y aller tout le monde, sinon ya que 3 personnes qui vont comprendre

On peut même tenter la news linuxfr car le sujet est clairement ardu et seul les courageux viendront ;-)

--
Vous recevez ce message, car vous êtes abonné au groupe Google Groupes Nantes FP.
Cette discussion peut être lue sur le Web à l'adresse https://groups.google.com/d/msg/nantes-fp/-/4JyU9GutumAJ.
Pour envoyer un message à ce groupe, adressez un e-mail à nant...@googlegroups.com.
Pour vous désabonner de ce groupe, envoyez un e-mail à l'adresse nantes-fp+...@googlegroups.com.
Pour plus d'options, consultez la page de ce groupe : http://groups.google.com/group/nantes-fp?hl=fr

--
---------------------
https://twitter.com/#!/ontologiae/
http://linuxfr.org/users/montaigne

[Albert]

Bonjour,

Effectivement, c'est intéressant.
2a et 2b tant qu'à faire et 2 séances c'est peut être même préférable pour 'digérer' les différents éléments.

Ensuite, si possible pas avant fin octobre me concernant (w44).

Cdt,

Albert.

---

De: "Pierre-Alexandre Voye" <ontol...@gmail.com>
À: nant...@googlegroups.com
Envoyé: Jeudi 11 Octobre 2012 16:55:38
Objet: Re: Proposition pour la prochaine séance : l'assistant de preuves formelles Coq

[Nicolas Rey]

Peu de chance que je sois encore à Nantes lorsque ça aura lieu, mais 2a et 2b m'intéresseraient bien !

Nicolas REY

[Mogzor]

2a et 2b aussi pour ma part, en deux séances, plutôt après les
vacances de toussaint si y a moyen pour moi.

Et super comme idée de conf :)

Hugo

2012/10/11 Nicolas Rey <nicolas...@gmail.com>:

[Rodolphe BELOUIN]

Je rejoins tout le monde, il serait dommage de sacrifier une des présentations alors qu'elles sont toutes les deux intéressantes.

Sinon je ne suis jamais disponible le lundi soir.

[Clement Delafargue]

Pareil, pour moi, super intéressé par 2a et 2b.

Cordialement,
Clément Delafargue
cle...@delafargue.name
http://www.eklaweb.com

PGP Fingerprint : 5311 A6C4 8416 5378 3019 B977 FFB4 9299 EAE0 ED53

Le 12 octobre 2012 08:54, Mogzor <mog...@gmail.com> a écrit :

[Pierre-Alexandre Voye]

Pareil pour moi, le pauvre homme va donc devoir faire les deux présentations ;-)

[Pierre-Alexandre Voye]

J'ai créé un doodle avec une date bidon pour savoir qui veut participer.

On va essayer d'avoir la possibilité de faire ça à la cantine, ce qui réduira les possibilités quand aux dates.

Maxime, quand serais-tu plutôt disponible ?
De même pour les autres ?

Le doodle :
http://www.doodle.com/wz7fcn6fb8b8uqm2

Le 12 octobre 2012 10:37, Clement Delafargue <cle...@delafargue.name> a écrit :

[Maxime Folschette]

Merci à tous pour votre enthousiasme ! Faire plusieurs séances ne sera pas un gros problème, ça permettra de mieux répartir le contenu.
Merci Pierre-Alexandre d'avoir relancé le truc, et désolé pour mon temps de réponse.

Le mieux serait de savoir quand la cantine sera disponible, ça sera peut-être le facteur le plus limitant.
Personnellement, je suis pour le moment disponible tous les soirs de semaine à partir du lundi 5 novembre (exception faite des vendredis soirs, qui ne naturellement pas partie de la semaine).

Je pense finalement faire trois séances puisque tout le monde semble intéressé par chaque sujet.

La première séance sera axée sur la présentation de Coq : généralités, utilisation, et un petit lot d'exemples et de preuves relativement simples pour comprendre le fonctionnement de la bête. Au niveau du format, je propose de faire une séance un peu hybride : le rythme sera assez lent pour que tout le monde puisse réécrire, tester et réfléchir aux exemples proposés sur sa machine personnelle, mais ça se sera pas une obligation pour pouvoir profiter de la séance car les exemples seront projetés et testés en direct. Je vous toucherai un mot sur la mise ne place d'un environnement Coq prochainement. Enfin, pour les intéressés qui ne pourront pas être là, je pourrai laisser mes notes en ligne.

Seul problème : je n'ai plus d'ordinateur portable, il faudrait donc qu'on me prête une machine le temps du séminaire, sur laquelle je sois en mesure d'installer mon environnement Coq.

À voir donc quand la Cantine serait disponible.
Je continue à bosser sur le cours en attendant.

Maxime

[Simon Thépot]

Bonjour,

ca fait un certain temps que je suis la mailing list mais je n'interviens pas car hélas, tous mes jeudis soirs sont pris (et qui plus est je n'ai pas un gros background théorique à faire partager, je code en python/js et je suis venu naturellement vers le paradigme fonctionnel qui semble très convaincant).

Je me mets sur le doodle mais à moins que ca ne se passe la semaine prochaine (ou je n'ai pas cours de ahem.. salsa !),

je ne pourrai pas venir, à mon grand regret.

En tout cas, joli sujet !

Merci,

Simon

[Clement Delafargue]

Hop,

Désolé pour le silence radio, j'ai un peu eu la tête sous l'eau ces derniers temps.

Je propose la date du 27 novembre qui est libre sur le calendrier de la cantine.
Si cela va à tout le monde, je réserve auprès de la Cantine.

Cheers,
Clément

[Pierre-Alexandre Voye]

Ok pour moi

Cette discussion peut être lue sur le Web à l'adresse https://groups.google.com/d/msg/nantes-fp/-/IDdBVSChjlwJ.

Pour envoyer un message à ce groupe, adressez un e-mail à nant...@googlegroups.com.
Pour vous désabonner de ce groupe, envoyez un e-mail à l'adresse nantes-fp+...@googlegroups.com.
Pour plus d'options, consultez la page de ce groupe : http://groups.google.com/group/nantes-fp?hl=fr

[Maxime Folschette]

Salut,

Ce n'est pas la date qui m'arrange le plus, mais comme l'agenda de la Cantine doit être plutôt bien chargé, je prends.
En plus c'est un mardi, ce qui pourra arranger plus de monde.

Maxime

[Clement Delafargue]

Ok. J'envoie l'email en fin d'aprèm, histoire d'attendre d'autres réponses.

Cordialement,
Clément Delafargue
cle...@delafargue.name
http://www.eklaweb.com

PGP Fingerprint : 5311 A6C4 8416 5378 3019  B977 FFB4 9299 EAE0 ED53

2012/11/16 Maxime Folschette <maxime.f...@gmail.com>

Cette discussion peut être lue sur le Web à l'adresse https://groups.google.com/d/msg/nantes-fp/-/7YPlZEkRrDQJ.

[Jonathan Winandy]

C'est bon pour le mardi 27 nov ? 

Jon

[Clément Delafargue]

Ça a l'air d'aller à tout le monde, donc oui.
J'envoie un email à Magali DQP.

Clément

Jonathan Winandy wrote:
> C'est bon pour le mardi 27 nov ?
>
> Jon
>
> Le vendredi 16 novembre 2012 15:02:10 UTC+1, Clement Delafargue a écrit :
> >
> > Ok. J'envoie l'email en fin d'aprèm, histoire d'attendre d'autres réponses.
> >
> > Cordialement,
> > Clément Delafargue

> > cle...@delafargue.name <javascript:>

> > http://www.eklaweb.com
> >
> > PGP Fingerprint : 5311 A6C4 8416 5378 3019 B977 FFB4 9299 EAE0 ED53
> >
> >

> > 2012/11/16 Maxime Folschette <maxime.f...@gmail.com <javascript:>>

> >>>>>>> http://www.doodle.com/**wz7fcn6f**b8b8uqm2<http://www.doodle.com/wz7fcn6fb8b8uqm2>

> >>>>>>>> >>> ______________________________****__

> >>>>>>>> >>>> [2] http://www.cis.upenn.edu/~**bcpi**erce/sf/<http://www.cis.upenn.edu/~bcpierce/sf/>
> >>>>>>>> >>>> [3] https://fr.wikipedia.org/wiki/****
> >>>>>>>> Th%C3%A9or%C3%A8me_des_quatre_****couleurs<https://fr.wikipedia.org/wiki/Th%C3%A9or%C3%A8me_des_quatre_couleurs>
> >>>>>>>> >>>> [4] http://www.labri.fr/perso/**cast**eran/CoqArt/index.html<http://www.labri.fr/perso/casteran/CoqArt/index.html>

> >>>>>>>> >>>>
> >>>>>>>> >>>> --
> >>>>>>>> >>>> Vous recevez ce message, car vous êtes abonné au groupe Google
> >>>>>>>> Groupes
> >>>>>>>> >>>> Nantes FP.
> >>>>>>>> >>>> Cette discussion peut être lue sur le Web à l'adresse

> >>>>>>>> >>>> https://groups.google.com/d/**ms**g/nantes-fp/-/4JyU9GutumAJ<https://groups.google.com/d/msg/nantes-fp/-/4JyU9GutumAJ>
> >>>>>>>> .

> >>>>>>>> >>>> Pour envoyer un message à ce groupe, adressez un e-mail à
> >>>>>>>> >>>> nant...@googlegroups.com.
> >>>>>>>> >>>> Pour vous désabonner de ce groupe, envoyez un e-mail à
> >>>>>>>> l'adresse

> >>>>>>>> >>>> nantes-fp+...@googlegroups.com****.

> >>>>>>>> >>>> Pour plus d'options, consultez la page de ce groupe :

> >>>>>>>> >>>> http://groups.google.com/**group**/nantes-fp?hl=fr<http://groups.google.com/group/nantes-fp?hl=fr>
> >>>>>>>> >>>
> >>>>>>>> >>>
> >>>>>>>> >>>
> >>>>>>>> >>>
> >>>>>>>> >>> --
> >>>>>>>> >>> ---------------------
> >>>>>>>> >>> https://twitter.com/#!/**ontolog**iae/<https://twitter.com/#!/ontologiae/>
> >>>>>>>> >>> http://linuxfr.org/users/**monta**igne<http://linuxfr.org/users/montaigne>

> >>>>>>>> >>>
> >>>>>>>> >>> --
> >>>>>>>> >>> Vous recevez ce message, car vous êtes abonné au groupe Google
> >>>>>>>> Groupes
> >>>>>>>> >>> Nantes FP.
> >>>>>>>> >>> Pour envoyer un message à ce groupe, adressez un e-mail à
> >>>>>>>> >>> nant...@googlegroups.com.
> >>>>>>>> >>> Pour vous désabonner de ce groupe, envoyez un e-mail à l'adresse

> >>>>>>>> >>> nantes-fp+...@googlegroups.com****.

> >>>>>>>> >>> Pour plus d'options, consultez la page de ce groupe :

> >>>>>>>> >>> http://groups.google.com/**group**/nantes-fp?hl=fr<http://groups.google.com/group/nantes-fp?hl=fr>

> >>>>>>>> >>>
> >>>>>>>> >>> --
> >>>>>>>> >>> Vous recevez ce message, car vous êtes abonné au groupe Google
> >>>>>>>> Groupes
> >>>>>>>> >>> Nantes FP.
> >>>>>>>> >>> Pour envoyer un message à ce groupe, adressez un e-mail à
> >>>>>>>> >>> nant...@googlegroups.com.
> >>>>>>>> >>> Pour vous désabonner de ce groupe, envoyez un e-mail à l'adresse

> >>>>>>>> >>> nantes-fp+...@googlegroups.com****.

> >>>>>>>> >>> Pour plus d'options, consultez la page de ce groupe :

> >>>>>>>> >>> http://groups.google.com/**group**/nantes-fp?hl=fr<http://groups.google.com/group/nantes-fp?hl=fr>

> >>>>>>>> >>
> >>>>>>>> >>
> >>>>>>>> >> --
> >>>>>>>> >> Vous recevez ce message, car vous êtes abonné au groupe Google
> >>>>>>>> Groupes
> >>>>>>>> >> Nantes FP.
> >>>>>>>> >> Pour envoyer un message à ce groupe, adressez un e-mail à
> >>>>>>>> >> nant...@googlegroups.com.
> >>>>>>>> >> Pour vous désabonner de ce groupe, envoyez un e-mail à l'adresse

> >>>>>>>> >> nantes-fp+...@googlegroups.com****.

> >>>>>>>> >> Pour plus d'options, consultez la page de ce groupe :

> >>>>>>>> >> http://groups.google.com/**group**/nantes-fp?hl=fr<http://groups.google.com/group/nantes-fp?hl=fr>

> >>>>>>>> >
> >>>>>>>> > --
> >>>>>>>> > Vous recevez ce message, car vous êtes abonné au groupe Google
> >>>>>>>> Groupes Nantes FP.
> >>>>>>>> > Pour envoyer un message à ce groupe, adressez un e-mail à
> >>>>>>>> nant...@googlegroups.com.
> >>>>>>>> > Pour vous désabonner de ce groupe, envoyez un e-mail à l'adresse

> >>>>>>>> nantes-fp+...@googlegroups.com****.

> >>>>>>>> > Pour plus d'options, consultez la page de ce groupe :

> >>>>>>>> http://groups.google.com/**group**/nantes-fp?hl=fr<http://groups.google.com/group/nantes-fp?hl=fr>

> >>>>>>>> >
> >>>>>>>>
> >>>>>>>> --
> >>>>>>>> Vous recevez ce message, car vous êtes abonné au groupe Google
> >>>>>>>> Groupes Nantes FP.
> >>>>>>>> Pour envoyer un message à ce groupe, adressez un e-mail à
> >>>>>>>> nant...@googlegroups.com.
> >>>>>>>> Pour vous désabonner de ce groupe, envoyez un e-mail à l'adresse

> >>>>>>>> nantes-fp+...@googlegroups.com****.

> >>>>>>>> Pour plus d'options, consultez la page de ce groupe :

> >>>>>>>> http://groups.google.com/**group**/nantes-fp?hl=fr<http://groups.google.com/group/nantes-fp?hl=fr>
> >>>>>>>>
> >>>>>>>>
> >>>>>>>
> >>>>>>>
> >>>>>>> --
> >>>>>>> ---------------------
> >>>>>>> https://twitter.com/#!/**ontolog**iae/<https://twitter.com/#%21/ontologiae/>
> >>>>>>> http://linuxfr.org/users/**monta**igne<http://linuxfr.org/users/montaigne>

> >>>>>>>
> >>>>>>> --
> >>>> Vous recevez ce message, car vous êtes abonné au groupe Google
> >>>> Groupes Nantes FP.
> >>>> Cette discussion peut être lue sur le Web à l'adresse

> >>>> https://groups.google.com/d/**msg/nantes-fp/-/IDdBVSChjlwJ<https://groups.google.com/d/msg/nantes-fp/-/IDdBVSChjlwJ>
> >>>> .

> >>>>
> >>>> Pour envoyer un message à ce groupe, adressez un e-mail à
> >>>> nant...@googlegroups.com.
> >>>> Pour vous désabonner de ce groupe, envoyez un e-mail à l'adresse

> >>>> nantes-fp+...@**googlegroups.com.

> >>>> Pour plus d'options, consultez la page de ce groupe :

> >>>> http://groups.google.com/**group/nantes-fp?hl=fr<http://groups.google.com/group/nantes-fp?hl=fr>
> >>>>
> >>>
> >>>
> >>>
> >>> --
> >>> ---------------------
> >>> https://twitter.com/#!/**ontologiae/<https://twitter.com/#%21/ontologiae/>
> >>> http://linuxfr.org/users/**montaigne<http://linuxfr.org/users/montaigne>

> >>>
> >>> --
> >> Vous recevez ce message, car vous êtes abonné au groupe Google
> >> Groupes Nantes FP.
> >> Cette discussion peut être lue sur le Web à l'adresse
> >> https://groups.google.com/d/msg/nantes-fp/-/7YPlZEkRrDQJ.
> >>
> >> Pour envoyer un message à ce groupe, adressez un e-mail à

> >> nant...@googlegroups.com <javascript:>.

> >> Pour vous désabonner de ce groupe, envoyez un e-mail à l'adresse

> >> nantes-fp+...@googlegroups.com <javascript:>.

> >> Pour plus d'options, consultez la page de ce groupe :
> >> http://groups.google.com/group/nantes-fp?hl=fr
> >>
> >
> >
>
> --
> Vous recevez ce message, car vous êtes abonné au groupe Google Groupes Nantes FP.

> Cette discussion peut être lue sur le Web à l'adresse https://groups.google.com/d/msg/nantes-fp/-/nKXgMejAM3wJ.

[Clément Delafargue]

J'ai eu Magali, la salle habituelle n'est *a priori* pas dispo, mais le nouvel
espace de coworking devrait l'être. Par contre il n'y a pas de vidéoproj là bas.

Clément

[Clément Delafargue]

J'ai eu Magali, elle nous a réservé le créneau et mis ça dans l'agenda de la
cantine.

On n'aura pas de vidéoproj mais un écran, ça devrait suffire.

Clément

[Clément Delafargue]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Voilà, j'ai créé un bidule eventbrite pour track les gens qui viennent.

http://nantesfp-coq.eventbrite.com/

-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.19 (GNU/Linux)

iQIcBAEBAgAGBQJQqmkrAAoJEGv+hjwmhK0JrBYQAJ2pwCIoWOliJDuSQfn34V7O
u3kTIdGVKF0O2ODmlRtcfw4ZZchtg2JJN29H26PqqljYm8NaCYA4lnPFwqVPKvWd
VG9zxDquZ4R5k7pfw/qwSoxwmqTBfWx/qwAIDGOFliu0VdBQe7beRL0/ItzlOLyc
jOKMeSkkixUqmMLDSoaWumqitZ/xMyXDBJ8xeURoSb6b9XCFUbPp+7cD+PvMcN2V
Nstku8cAma6fVtSJ1gSw7EZpP4iqHOu954qgDKB5S6g72OguwCn7GVibzUtmW0Ey
Ds5cGkKPKAtL4sPGZGzaGOZBizRZ5Qhq9Vs7P+8nGLq+ksyXdV2tXBNzlKn+p4EG
/Zhdd3t6SaotjDInlXpJQZv18i9fGQQwMDpP6gV9VcB5ckUROZJZC7CltzJ1RXa+
AxFAthHFgILRGWJslrJ3S7X4FbApz+o0R2nAYuc6XNQXZeDiyitJEGGUDDfw2hXQ
gOcplBxLFHVVtikaw3MNZbrjDrtMn52UBkTVdfOfqDBuaYs6EhmiJXsc4EdFqNRA
81J6u5P2uDHe6Utm4bQyuGVz+1njMi6zFHvhecppEexv/BzJ25MwLREysMOz7R7o
y77Csg3Uw6v0ZQhZBnQGe5oqjrIU76QiqtnZzLQGuDXWRZCDcM+7xB4ZB2N13l65
HFrcOrwH2h5eSatfjAYX
=91KN
-----END PGP SIGNATURE-----

[Albert]

Bonjour,

Les mardi, perso, je ne peux pas. Mais je peux toujours récupérer les slides après ;)

Albert

---

De: "Clement Delafargue" <cle...@delafargue.name>
À: nant...@googlegroups.com
Envoyé: Vendredi 16 Novembre 2012 15:01:47

[Cédric Pineau]

Je ne sais pas si c'est prévu, mais une petite introduction permettant de placer Coq au sein du mouvement plus global que je crois deviner au travers de cet article par exemple serait vraiment top :-)

http://www.dzone.com/links/r/unifying_programming_and_math_the_dependent_type.html

Cédric

Cédric

[Mogzor]

c'est très bien pour moi aussi.

2012/11/16 Pierre-Alexandre Voye <ontol...@gmail.com>:

[Rodolphe BELOUIN]

Ok :)

2012/11/16 Pierre-Alexandre Voye <ontol...@gmail.com>

[Pierre-Alexandre Voye]

Ok, dès que tu confirmes, je créé une news linuxfr

[Pierre-Alexandre Voye]

Ya une limite en taille pour la salle ? C'est pour la news Linuxfr..

[Cédric Pineau]

Pour moi aussi, même si je ne me suis pas manifesté jusqu'à maintenant !

Cédric

Cédric

[Clément Delafargue]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Google groups avait gardé 7 messages en spam, sans prévenir… Désolé pour le
contretemps.

@PA: je demande à Magali pour la taille de la salle

@Albert: désolé, je viens juste de voir ton mail, on mettra bien entendu les
slides à dispo, ainsi que le code tapé.

Clément


Cédric Pineau wrote:
> Je ne sais pas si c'est prA(c)vu, mais une petite introduction permettant

> de placer Coq au sein du mouvement plus global que je crois deviner au
> travers de cet article par exemple serait vraiment top :-)
>
> http://www.dzone.com/links/r/unifying_programming_and_math_the_dependent_type.html
>

> CA(c)dric
>
> Le 19 novembre 2012 18:15, ClA(c)ment Delafargue <cle...@delafargue.name>
> a A(c)crit :

>
> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA1
>

> VoilA , j'ai crA(c)A(c) un bidule eventbrite pour track les gens qui
> viennent.
>
> http://nantesfp-coq.eventbrite.com/
> ClA(c)ment
>
> ClA(c)ment Delafargue wrote:
> > J'ai eu Magali, elle nous a rA(c)servA(c) le crA(c)neau et mis AS:a

> dans l'agenda de la
> > cantine.
> >

> > On n'aura pas de vidA(c)oproj mais un A(c)cran, AS:a devrait suffire.
> >
> > ClA(c)ment

> >
> > ClA(c)ment Delafargue wrote:
> > > J'ai eu Magali, la salle habituelle n'est *a priori* pas dispo, mais
> le nouvel

> > > espace de coworking devrait l'A-atre. Par contre il n'y a pas de
> vidA(c)oproj lA bas.
> > >
> > > ClA(c)ment
> > >
> > > ClA(c)ment Delafargue wrote:
> > > > A*a a l'air d'aller A tout le monde, donc oui.
> > > > J'envoie un email A Magali DQP.
> > > >
> > > > ClA(c)ment

> > > > Jonathan Winandy wrote:
> > > > > C'est bon pour le mardi 27 nov ?
> > > > >
> > > > > Jon
> > > > >
> > > > > Le vendredi 16 novembre 2012 15:02:10 UTC+1, Clement Delafargue

> a A(c)crit :
> > > > > >
> > > > > > Ok. J'envoie l'email en fin d'aprA"m, histoire d'attendre
> d'autres rA(c)ponses.
> > > > > >
> > > > > > Cordialement,
> > > > > > ClA(c)ment Delafargue
> > > > > > cle...@delafargue.name <javascript:>
> > > > > > http://www.eklaweb.com
> > > > > >
> > > > > > PGP Fingerprint : 5311 A6C4 8416 5378 3019 A B977 FFB4 9299

> EAE0 ED53
> > > > > >
> > > > > >
> > > > > > 2012/11/16 Maxime Folschette <maxime.f...@gmail.com
> <javascript:>>
> > > > > >
> > > > > >> Salut,
> > > > > >>
> > > > > >> Ce n'est pas la date qui m'arrange le plus, mais comme
> l'agenda de la

> > > > > >> Cantine doit A-atre plutA't bien chargA(c), je prends.

> > > > > >> En plus c'est un mardi, ce qui pourra arranger plus de monde.
> > > > > >>
> > > > > >> Maxime
> > > > > >>
> > > > > >>
> > > > > >>
> > > > > >> On Friday, November 16, 2012 2:08:52 PM UTC+1,
> Pierre-Alexandre Voye
> > > > > >> wrote:
> > > > > >>
> > > > > >>> Ok pour moi
> > > > > >>>
> > > > > >>>
> > > > > >>> Le 16 novembre 2012 14:04, Clement Delafargue
> <diva...@gmail.com> a

> > > > > >>> A(c)crit :
> > > > > >>>
> > > > > >>> Hop,
> > > > > >>>>
> > > > > >>>> DA(c)solA(c) pour le silence radio, j'ai un peu eu la
> tA-ate sous l'eau ces

> > > > > >>>> derniers temps.
> > > > > >>>>
> > > > > >>>> Je propose la date du 27 novembre qui est libre sur le
> calendrier de la
> > > > > >>>> cantine.

> > > > > >>>> Si cela va A tout le monde, je rA(c)serve auprA"s de la
> Cantine.
> > > > > >>>>
> > > > > >>>> Cheers,
> > > > > >>>> ClA(c)ment

> > > > > >>>>
> > > > > >>>>
> > > > > >>>> On Tuesday, October 30, 2012 8:45:10 AM UTC+1, Simon

> ThA(c)pot wrote:
> > > > > >>>>>
> > > > > >>>>> Bonjour,
> > > > > >>>>>
> > > > > >>>>> ca fait un certain temps que je suis la mailing list mais
> je

> > > > > >>>>> n'interviens pas car hA(c)las, tous mes jeudis soirs sont
> pris (et qui plus
> > > > > >>>>> est je n'ai pas un gros background thA(c)orique A faire

> partager, je code en
> > > > > >>>>> python/js et je suis venu naturellement vers le paradigme
> fonctionnel qui

> > > > > >>>>> semble trA"s convaincant).
> > > > > >>>>> Je me mets sur le doodle mais A moins que ca ne se passe

> la semaine
> > > > > >>>>> prochaine (ou je n'ai pas cours de ahem.. salsa !),

> > > > > >>>>> je ne pourrai pas venir, A mon grand regret.

> > > > > >>>>>
> > > > > >>>>> En tout cas, joli sujet !
> > > > > >>>>> Merci,
> > > > > >>>>>
> > > > > >>>>> Simon
> > > > > >>>>>
> > > > > >>>>> Le lundi 29 octobre 2012 21:28:44 UTC+1, Maxime Folschette

> a A(c)crit :
> > > > > >>>>>>
> > > > > >>>>>> Merci A tous pour votre enthousiasmea*-! Faire plusieurs
> sA(c)ances ne
> > > > > >>>>>> sera pas un gros problA"me, AS:a permettra de mieux
> rA(c)partir le contenu.
> > > > > >>>>>> Merci Pierre-Alexandre d'avoir relancA(c) le truc, et
> dA(c)solA(c) pour mon
> > > > > >>>>>> temps de rA(c)ponse.

> > > > > >>>>>>
> > > > > >>>>>> Le mieux serait de savoir quand la cantine sera

> disponible, AS:a sera
> > > > > >>>>>> peut-A-atre le facteur le plus limitant.

> > > > > >>>>>> Personnellement, je suis pour le moment disponible tous
> les soirs de

> > > > > >>>>>> semaine A partir du lundi 5 novembre (exception faite

> des vendredis soirs,
> > > > > >>>>>> qui ne naturellement pas partie de la semaine).
> > > > > >>>>>>

> > > > > >>>>>> Je pense finalement faire trois sA(c)ances puisque tout
> le monde semble
> > > > > >>>>>> intA(c)ressA(c) par chaque sujet.
> > > > > >>>>>>
> > > > > >>>>>> La premiA"re sA(c)ance sera axA(c)e sur la
> prA(c)sentation de Coqa*-:
> > > > > >>>>>> gA(c)nA(c)ralitA(c)s, utilisation, et un petit lot

> d'exemples et de preuves
> > > > > >>>>>> relativement simples pour comprendre le fonctionnement de

> la bA-ate. Au
> > > > > >>>>>> niveau du format, je propose de faire une sA(c)ance un
> peu hybridea*-: le rythme

> > > > > >>>>>> sera assez lent pour que tout le monde puisse

> rA(c)A(c)crire, tester et rA(c)flA(c)chir
> > > > > >>>>>> aux exemples proposA(c)s sur sa machine personnelle, mais
> AS:a se sera pas une
> > > > > >>>>>> obligation pour pouvoir profiter de la sA(c)ance car les
> exemples seront
> > > > > >>>>>> projetA(c)s et testA(c)s en direct. Je vous toucherai un

> mot sur la mise ne place
> > > > > >>>>>> d'un environnement Coq prochainement. Enfin, pour les

> intA(c)ressA(c)s qui ne
> > > > > >>>>>> pourront pas A-atre lA , je pourrai laisser mes notes en
> ligne.
> > > > > >>>>>>
> > > > > >>>>>> Seul problA"mea*-: je n'ai plus d'ordinateur portable, il
> faudrait donc
> > > > > >>>>>> qu'on me prA-ate une machine le temps du sA(c)minaire,

> sur laquelle je sois en
> > > > > >>>>>> mesure d'installer mon environnement Coq.
> > > > > >>>>>>

> > > > > >>>>>> A* voir donc quand la Cantine serait disponible.
> > > > > >>>>>> Je continue A bosser sur le cours en attendant.

> > > > > >>>>>>
> > > > > >>>>>> Maxime
> > > > > >>>>>>
> > > > > >>>>>>
> > > > > >>>>>> Le lundi 22 octobre 2012 16:18:40 UTC+2, Pierre-Alexandre
> Voye a

> > > > > >>>>>> A(c)crit :
> > > > > >>>>>>>
> > > > > >>>>>>> J'ai crA(c)A(c) un doodle avec une date bidon pour
> savoir qui veut
> > > > > >>>>>>> participer.
> > > > > >>>>>>>
> > > > > >>>>>>> On va essayer d'avoir la possibilitA(c) de faire AS:a A
> la cantine, ce
> > > > > >>>>>>> qui rA(c)duira les possibilitA(c)s quand aux dates.
> > > > > >>>>>>>
> > > > > >>>>>>> Maxime, quand serais-tu plutA't disponible ?
> > > > > >>>>>>> De mA-ame pour les autres ?

> > > > > >>>>>>>
> > > > > >>>>>>> Le doodle :
> > > > > >>>>>>>
> http://www.doodle.com/**wz7fcn6f**b8b8uqm2<http://www.doodle.com/wz7fcn6fb8b8uqm2>
> > > > > >>>>>>>
> > > > > >>>>>>> Le 12 octobre 2012 10:37, Clement Delafargue
> <cle...@delafargue.name

> > > > > >>>>>>> > a A(c)crit :
> > > > > >>>>>>>
> > > > > >>>>>>>> Pareil, pour moi, super intA(c)ressA(c) par 2a et 2b.
> > > > > >>>>>>>>
> > > > > >>>>>>>> Cordialement,
> > > > > >>>>>>>> ClA(c)ment Delafargue
> > > > > >>>>>>>> cle...@delafargue.name
> > > > > >>>>>>>> http://www.eklaweb.com
> > > > > >>>>>>>>
> > > > > >>>>>>>> PGP Fingerprint : 5311 A6C4 8416 5378 3019 A B977 FFB4

> 9299 EAE0 ED53
> > > > > >>>>>>>>
> > > > > >>>>>>>>
> > > > > >>>>>>>> Le 12 octobre 2012 08:54, Mogzor <mog...@gmail.com> a

> A(c)crit :
> > > > > >>>>>>>> > 2a et 2b aussi pour ma part, en deux sA(c)ances,
> plutA't aprA"s les

> > > > > >>>>>>>> > vacances de toussaint si y a moyen pour moi.
> > > > > >>>>>>>> >

> > > > > >>>>>>>> > Et super comme idA(c)e de conf :)

> > > > > >>>>>>>> >
> > > > > >>>>>>>> > Hugo
> > > > > >>>>>>>> >
> > > > > >>>>>>>> > 2012/10/11 Nicolas Rey <nicolas...@gmail.com>:

> > > > > >>>>>>>> >> Peu de chance que je sois encore A Nantes lorsque
> AS:a aura lieu,
> > > > > >>>>>>>> mais 2a et
> > > > > >>>>>>>> >> 2b m'intA(c)resseraient bien !

> > > > > >>>>>>>> >>
> > > > > >>>>>>>> >> Nicolas REY
> > > > > >>>>>>>> >>
> > > > > >>>>>>>> >>
> > > > > >>>>>>>> >> Le 11 octobre 2012 17:12, Albert

> <alber...@see4sys.com> a A(c)crit
> > > > > >>>>>>>> :
> > > > > >>>>>>>> >>
> > > > > >>>>>>>> >>> Bonjour,
> > > > > >>>>>>>> >>>
> > > > > >>>>>>>> >>> Effectivement, c'est intA(c)ressant.
> > > > > >>>>>>>> >>> 2a et 2b tant qu'A faire et 2 sA(c)ances c'est
> peut A-atre mA-ame
> > > > > >>>>>>>> prA(c)fA(c)rable pour
> > > > > >>>>>>>> >>> 'digA(c)rer' les diffA(c)rents A(c)lA(c)ments.

> > > > > >>>>>>>> >>>
> > > > > >>>>>>>> >>> Ensuite, si possible pas avant fin octobre me
> concernant (w44).
> > > > > >>>>>>>> >>>
> > > > > >>>>>>>> >>> Cdt,
> > > > > >>>>>>>> >>>
> > > > > >>>>>>>> >>> Albert.
> > > > > >>>>>>>> >>>
> > > > > >>>>>>>> >>> ______________________________****__
> > > > > >>>>>>>> >>> De: "Pierre-Alexandre Voye" <ontol...@gmail.com>

> > > > > >>>>>>>> >>> A*: nant...@googlegroups.com
> > > > > >>>>>>>> >>> EnvoyA(c): Jeudi 11 Octobre 2012 16:55:38
> > > > > >>>>>>>> >>> Objet: Re: Proposition pour la prochaine sA(c)ance

> : l'assistant
> > > > > >>>>>>>> de preuves
> > > > > >>>>>>>> >>> formelles Coq
> > > > > >>>>>>>> >>>
> > > > > >>>>>>>> >>>

> > > > > >>>>>>>> >>> Moi AS:a me tente parce que AS:a fait 10 ans que je
> tourne autour
> > > > > >>>>>>>> sans jamais
> > > > > >>>>>>>> >>> m'y mettre sA(c)rieusement.

> > > > > >>>>>>>> >>> C'est passionnant et c'est important de

> sensibiliser les gens A
> > > > > >>>>>>>> AS:a.
> > > > > >>>>>>>> >>> AprA"s je pense qu'il va falloir y aller tout le

> monde, sinon ya
> > > > > >>>>>>>> que 3
> > > > > >>>>>>>> >>> personnes qui vont comprendre
> > > > > >>>>>>>> >>>

> > > > > >>>>>>>> >>> On peut mA-ame tenter la news linuxfr car le sujet

> est clairement
> > > > > >>>>>>>> ardu et
> > > > > >>>>>>>> >>> seul les courageux viendront ;-)
> > > > > >>>>>>>> >>>
> > > > > >>>>>>>> >>> Le 11 octobre 2012 16:48, Maxime Folschette <
> > > > > >>>>>>>> maxime.f...@gmail.com>

> > > > > >>>>>>>> >>> a A(c)crit :
> > > > > >>>>>>>> >>>>
> > > > > >>>>>>>> >>>> Bonjour A tous,
> > > > > >>>>>>>> >>>>
> > > > > >>>>>>>> >>>> Pour la prochaine sA(c)ance du Nantes FP Group et
> aprA"s
> > > > > >>>>>>>> discussion avec
> > > > > >>>>>>>> >>>> ClA(c)ment, je vous propose une sA(c)ance autour

> de Coq [1], qui est
> > > > > >>>>>>>> un assistant
> > > > > >>>>>>>> >>>> de preuves formelles.

> > > > > >>>>>>>> >>>> Certains se demanderont peut-A-atre A premiA"re

> vue quel rapport
> > > > > >>>>>>>> cela pourra
> > > > > >>>>>>>> >>>> avoir avec la programmation fonctionnelle, mais le
> lien est en

> > > > > >>>>>>>> rA(c)alitA(c) trA"s
> > > > > >>>>>>>> >>>> A(c)troit.
> > > > > >>>>>>>> >>>>
> > > > > >>>>>>>> >>>> En quelques mots, Coq permet de dA(c)finir des
> objets
> > > > > >>>>>>>> mathA(c)matiques A l'aide

> > > > > >>>>>>>> >>>> du langage Gallina (qui est purement fonctionnel).
> Ces objets
> > > > > >>>>>>>> peuvent
> > > > > >>>>>>>> >>>> globalement prendre la forme de types, fonctions
> ou
> > > > > >>>>>>>> propositions

> > > > > >>>>>>>> >>>> mathA(c)matiques. Dans un deuxiA"me temps, Coq
> permet, A l'aide
> > > > > >>>>>>>> d'un
> > > > > >>>>>>>> >>>> environnement de dA(c)monstration bien fourni,

> d'effectuer la
> > > > > >>>>>>>> preuve des

> > > > > >>>>>>>> >>>> diverses propositions que vous avez avancA(c)es.
> > > > > >>>>>>>> >>>> Un exemple trA"s simple (et trA"s courant)

> d'utilisation de Coq,
> > > > > >>>>>>>> qui sera

> > > > > >>>>>>>> >>>> certainement le premier exemple de la sA(c)ance,
> est la
> > > > > >>>>>>>> dA(c)finition de

> > > > > >>>>>>>> >>>> l'ensemble des entiers naturels, puis la

> dA(c)finition de

> > > > > >>>>>>>> l'addition sur ces
> > > > > >>>>>>>> >>>> entiers. Par la suite, on pourra vouloir prouver
> sont la

> > > > > >>>>>>>> commutativitA(c) et
> > > > > >>>>>>>> >>>> l'associativitA(c) de cette opA(c)ration.
> > > > > >>>>>>>> >>>> L'utilisation de Coq peut aller trA"s loin. On

> peut notamment
> > > > > >>>>>>>> s'en servir

> > > > > >>>>>>>> >>>> pour prouver des programmes impA(c)ratifs A

> l'aide de logique de
> > > > > >>>>>>>> Hoare par

> > > > > >>>>>>>> >>>> exemple [2]. Il a aussi permis la dA(c)monstration
> de certains
> > > > > >>>>>>>> thA(c)orA"mes, donc
> > > > > >>>>>>>> >>>> le plus cA(c)lA"bre est le thA(c)orA"me des quatre
> couleurs [3].
> > > > > >>>>>>>> >>>>
> > > > > >>>>>>>> >>>> Son lien A(c)troit avec la programmation

> fonctionnelle, outre le
> > > > > >>>>>>>> langage
> > > > > >>>>>>>> >>>> Gallina, se situe au niveau d'une notion qu'on
> appelle
> > > > > >>>>>>>> l'isomorphisme de

> > > > > >>>>>>>> >>>> Curry-Howard, qui stipule la prA(c)sence d'une
> correspondance
> > > > > >>>>>>>> entre preuve et
> > > > > >>>>>>>> >>>> fonction mathA(c)matique. Cette correspondance est

> un peu
> > > > > >>>>>>>> subtile, mais je vous

> > > > > >>>>>>>> >>>> propose de la dA(c)couvrir au terme de cette
> sA(c)ance, ou d'une
> > > > > >>>>>>>> seconde sA(c)ance si
> > > > > >>>>>>>> >>>> nA(c)cessaire.

> > > > > >>>>>>>> >>>>
> > > > > >>>>>>>> >>>> Je vous propose donc le programme suivant (assez

> consA(c)quent)
> > > > > >>>>>>>> autour de
> > > > > >>>>>>>> >>>> Coqa*-:
> > > > > >>>>>>>> >>>> 1) Introduction A Coq et au langage de
> description Gallinaa*-:
> > > > > >>>>>>>> dA(c)finitions
> > > > > >>>>>>>> >>>> basiques d'objets mathA(c)matiques et utilisation
> de
> > > > > >>>>>>>> l'environnement de
> > > > > >>>>>>>> >>>> preuvesa*-;
> > > > > >>>>>>>> >>>> 2a) Preuve de programmes impA(c)ratifsa*-: aprA"s
> avoir dA(c)fini la
> > > > > >>>>>>>> grammaire et
> > > > > >>>>>>>> >>>> la sA(c)mantique d'un langage impA(c)ratif simple,

> il devient
> > > > > >>>>>>>> possible de prouver
> > > > > >>>>>>>> >>>> que celui-ci observe le comportement

> dA(c)sirA(c)a*-;
> > > > > >>>>>>>> >>>> 2b) PrA(c)sentation de l'isomorphisme de
> Curry-Howarda*-: il est

> > > > > >>>>>>>> possible de
> > > > > >>>>>>>> >>>> se passer de l'environnement de preuves de Coq et

> d'A(c)crire les
> > > > > >>>>>>>> preuves de
> > > > > >>>>>>>> >>>> thA(c)orA"mes sous forme de fonctions, leur
> correction A(c)tant
> > > > > >>>>>>>> assurA(c)e grA-c-ce au

> > > > > >>>>>>>> >>>> typage fort de Gallina.
> > > > > >>>>>>>> >>>>
> > > > > >>>>>>>> >>>> Ce programme se divise en deux branches (2a et 2b)
> qui ne sont
> > > > > >>>>>>>> pas

> > > > > >>>>>>>> >>>> antinomiques, mais qui auraient plutA't
> intA(c)rA-at A A-atre traitA(c)es
> > > > > >>>>>>>> sA(c)parA(c)ment.

> > > > > >>>>>>>> >>>> Je souhaiterais ainsi avoir un retour de votre
> part afin de

> > > > > >>>>>>>> savoira*-:
> > > > > >>>>>>>> >>>> a** d'une part si ce sujet vous intA(c)resse,
> > > > > >>>>>>>> >>>> a** d'autre part quel aspect (parmi 2a et 2b) vous
> prA(c)fA(c)reriez
> > > > > >>>>>>>> A(c)tudier
> > > > > >>>>>>>> >>>> (A<<a*-les deuxa*-A>> A(c)tant une rA(c)ponse tout
> A fait acceptable).
> > > > > >>>>>>>> >>>>
> > > > > >>>>>>>> >>>> Il restera aussi A discuter de la charge d'une
> telle sA(c)ance

> > > > > >>>>>>>> (il sera
> > > > > >>>>>>>> >>>> possible de la diviser si le sujet semble trop
> complexe pour

> > > > > >>>>>>>> A-atre traitA(c) en

> > > > > >>>>>>>> >>>> une fois), et naturellement de la date.
> > > > > >>>>>>>> >>>>

> > > > > >>>>>>>> >>>> Ceux qui sont curieux A propos de Coq pourront
> consulter un
> > > > > >>>>>>>> tutoriel [2]
> > > > > >>>>>>>> >>>> et un livre [4] A son propos.
> > > > > >>>>>>>> >>>>
> > > > > >>>>>>>> >>>> En attendant votre rA(c)ponse je vous souhaite une

> bonne fin de
> > > > > >>>>>>>> semaine,
> > > > > >>>>>>>> >>>>
> > > > > >>>>>>>> >>>> Maxime
> > > > > >>>>>>>> >>>>
> > > > > >>>>>>>> >>>>
> > > > > >>>>>>>> >>>> [1] http://coq.inria.fr/
> > > > > >>>>>>>> >>>> [2]
> http://www.cis.upenn.edu/~**bcpi**erce/sf/<http://www.cis.upenn.edu/~bcpierce/sf/>
> > > > > >>>>>>>> >>>> [3] https://fr.wikipedia.org/wiki/****
> > > > > >>>>>>>>
> Th%C3%A9or%C3%A8me_des_quatre_****couleurs<https://fr.wikipedia.org/wiki/Th%C3%A9or%C3%A8me_des_quatre_couleurs>
> > > > > >>>>>>>> >>>> [4]
> http://www.labri.fr/perso/**cast**eran/CoqArt/index.html<http://www.labri.fr/perso/casteran/CoqArt/index.html>
> > > > > >>>>>>>> >>>>
> > > > > >>>>>>>> >>>> --

> > > > > >>>>>>>> >>>> Vous recevez ce message, car vous A-ates abonnA(c)

> au groupe Google
> > > > > >>>>>>>> Groupes
> > > > > >>>>>>>> >>>> Nantes FP.

> > > > > >>>>>>>> >>>> Cette discussion peut A-atre lue sur le Web A

> l'adresse
> > > > > >>>>>>>> >>>>
> https://groups.google.com/d/**ms**g/nantes-fp/-/4JyU9GutumAJ<https://groups.google.com/d/msg/nantes-fp/-/4JyU9GutumAJ>
> > > > > >>>>>>>> .

> > > > > >>>>>>>> >>>> Pour envoyer un message A ce groupe, adressez un
> e-mail A
> > > > > >>>>>>>> >>>> nant...@googlegroups.com.
> > > > > >>>>>>>> >>>> Pour vous dA(c)sabonner de ce groupe, envoyez un
> e-mail A

> > > > > >>>>>>>> l'adresse
> > > > > >>>>>>>> >>>> nantes-fp+...@googlegroups.com****.
> > > > > >>>>>>>> >>>> Pour plus d'options, consultez la page de ce
> groupe :
> > > > > >>>>>>>> >>>>
> http://groups.google.com/**group**/nantes-fp?hl=fr<http://groups.google.com/group/nantes-fp?hl=fr>
> > > > > >>>>>>>> >>>
> > > > > >>>>>>>> >>>
> > > > > >>>>>>>> >>>
> > > > > >>>>>>>> >>>
> > > > > >>>>>>>> >>> --
> > > > > >>>>>>>> >>> ---------------------
> > > > > >>>>>>>> >>>
> https://twitter.com/#!/**ontolog**iae/<https://twitter.com/#!/ontologiae/>
> > > > > >>>>>>>> >>>
> http://linuxfr.org/users/**monta**igne<http://linuxfr.org/users/montaigne>
> > > > > >>>>>>>> >>>
> > > > > >>>>>>>> >>> --

> > > > > >>>>>>>> >>> Vous recevez ce message, car vous A-ates abonnA(c)

> au groupe Google
> > > > > >>>>>>>> Groupes
> > > > > >>>>>>>> >>> Nantes FP.

> > > > > >>>>>>>> >>> Pour envoyer un message A ce groupe, adressez un
> e-mail A
> > > > > >>>>>>>> >>> nant...@googlegroups.com.
> > > > > >>>>>>>> >>> Pour vous dA(c)sabonner de ce groupe, envoyez un
> e-mail A l'adresse

> > > > > >>>>>>>> >>> nantes-fp+...@googlegroups.com****.
> > > > > >>>>>>>> >>> Pour plus d'options, consultez la page de ce groupe
> :
> > > > > >>>>>>>> >>>
> http://groups.google.com/**group**/nantes-fp?hl=fr<http://groups.google.com/group/nantes-fp?hl=fr>
> > > > > >>>>>>>> >>>
> > > > > >>>>>>>> >>> --

> > > > > >>>>>>>> >>> Vous recevez ce message, car vous A-ates abonnA(c)

> au groupe Google
> > > > > >>>>>>>> Groupes
> > > > > >>>>>>>> >>> Nantes FP.

> > > > > >>>>>>>> >>> Pour envoyer un message A ce groupe, adressez un
> e-mail A
> > > > > >>>>>>>> >>> nant...@googlegroups.com.
> > > > > >>>>>>>> >>> Pour vous dA(c)sabonner de ce groupe, envoyez un
> e-mail A l'adresse

> > > > > >>>>>>>> >>> nantes-fp+...@googlegroups.com****.
> > > > > >>>>>>>> >>> Pour plus d'options, consultez la page de ce groupe
> :
> > > > > >>>>>>>> >>>
> http://groups.google.com/**group**/nantes-fp?hl=fr<http://groups.google.com/group/nantes-fp?hl=fr>
> > > > > >>>>>>>> >>
> > > > > >>>>>>>> >>
> > > > > >>>>>>>> >> --

> > > > > >>>>>>>> >> Vous recevez ce message, car vous A-ates abonnA(c)

> au groupe Google
> > > > > >>>>>>>> Groupes
> > > > > >>>>>>>> >> Nantes FP.

> > > > > >>>>>>>> >> Pour envoyer un message A ce groupe, adressez un
> e-mail A
> > > > > >>>>>>>> >> nant...@googlegroups.com.
> > > > > >>>>>>>> >> Pour vous dA(c)sabonner de ce groupe, envoyez un
> e-mail A l'adresse

> > > > > >>>>>>>> >> nantes-fp+...@googlegroups.com****.
> > > > > >>>>>>>> >> Pour plus d'options, consultez la page de ce groupe
> :
> > > > > >>>>>>>> >>
> http://groups.google.com/**group**/nantes-fp?hl=fr<http://groups.google.com/group/nantes-fp?hl=fr>
> > > > > >>>>>>>> >
> > > > > >>>>>>>> > --

> > > > > >>>>>>>> > Vous recevez ce message, car vous A-ates abonnA(c) au

> groupe Google
> > > > > >>>>>>>> Groupes Nantes FP.

> > > > > >>>>>>>> > Pour envoyer un message A ce groupe, adressez un
> e-mail A
> > > > > >>>>>>>> nant...@googlegroups.com.
> > > > > >>>>>>>> > Pour vous dA(c)sabonner de ce groupe, envoyez un
> e-mail A l'adresse

> > > > > >>>>>>>> nantes-fp+...@googlegroups.com****.
> > > > > >>>>>>>> > Pour plus d'options, consultez la page de ce groupe :
> > > > > >>>>>>>>
> http://groups.google.com/**group**/nantes-fp?hl=fr<http://groups.google.com/group/nantes-fp?hl=fr>
> > > > > >>>>>>>> >
> > > > > >>>>>>>>
> > > > > >>>>>>>> --

> > > > > >>>>>>>> Vous recevez ce message, car vous A-ates abonnA(c) au

> groupe Google
> > > > > >>>>>>>> Groupes Nantes FP.

> > > > > >>>>>>>> Pour envoyer un message A ce groupe, adressez un
> e-mail A
> > > > > >>>>>>>> nant...@googlegroups.com.
> > > > > >>>>>>>> Pour vous dA(c)sabonner de ce groupe, envoyez un e-mail
> A l'adresse

> > > > > >>>>>>>> nantes-fp+...@googlegroups.com****.
> > > > > >>>>>>>> Pour plus d'options, consultez la page de ce groupe :
> > > > > >>>>>>>>
> http://groups.google.com/**group**/nantes-fp?hl=fr<http://groups.google.com/group/nantes-fp?hl=fr>
> > > > > >>>>>>>>
> > > > > >>>>>>>>
> > > > > >>>>>>>
> > > > > >>>>>>>
> > > > > >>>>>>> --
> > > > > >>>>>>> ---------------------
> > > > > >>>>>>>
> https://twitter.com/#!/**ontolog**iae/<https://twitter.com/#%21/ontologiae/>
> > > > > >>>>>>>
> http://linuxfr.org/users/**monta**igne<http://linuxfr.org/users/montaigne>
> > > > > >>>>>>>

> > > > > >>>>>>> A --
> > > > > >>>> Vous recevez ce message, car vous A-ates abonnA(c) au

> groupe Google
> > > > > >>>> Groupes Nantes FP.

> > > > > >>>> Cette discussion peut A-atre lue sur le Web A l'adresse

> > > > > >>>>
> https://groups.google.com/d/**msg/nantes-fp/-/IDdBVSChjlwJ<https://groups.google.com/d/msg/nantes-fp/-/IDdBVSChjlwJ>
> > > > > >>>> .
> > > > > >>>>

> > > > > >>>> Pour envoyer un message A ce groupe, adressez un e-mail A
> > > > > >>>> nant...@googlegroups.com.
> > > > > >>>> Pour vous dA(c)sabonner de ce groupe, envoyez un e-mail A

> l'adresse
> > > > > >>>> nantes-fp+...@**googlegroups.com.
> > > > > >>>> Pour plus d'options, consultez la page de ce groupe :
> > > > > >>>>
> http://groups.google.com/**group/nantes-fp?hl=fr<http://groups.google.com/group/nantes-fp?hl=fr>
> > > > > >>>>
> > > > > >>>
> > > > > >>>
> > > > > >>>
> > > > > >>> --
> > > > > >>> ---------------------
> > > > > >>>
> https://twitter.com/#!/**ontologiae/<https://twitter.com/#%21/ontologiae/>
> > > > > >>>
> http://linuxfr.org/users/**montaigne<http://linuxfr.org/users/montaigne>
> > > > > >>>

> > > > > >>> A --
> > > > > >> Vous recevez ce message, car vous A-ates abonnA(c) au groupe
> Google
> > > > > >> Groupes Nantes FP.
> > > > > >> Cette discussion peut A-atre lue sur le Web A l'adresse
> > > > > >> https://groups.google.com/d/msg/nantes-fp/-/7YPlZEkRrDQJ.
> > > > > >>
> > > > > >> Pour envoyer un message A ce groupe, adressez un e-mail A
> > > > > >> nant...@googlegroups.com <javascript:>.
> > > > > >> Pour vous dA(c)sabonner de ce groupe, envoyez un e-mail A

> l'adresse
> > > > > >> nantes-fp+...@googlegroups.com <javascript:>.
> > > > > >> Pour plus d'options, consultez la page de ce groupe :
> > > > > >> http://groups.google.com/group/nantes-fp?hl=fr
> > > > > >>
> > > > > >
> > > > > >
> > > > >
> > > > > --

> > > > > Vous recevez ce message, car vous A-ates abonnA(c) au groupe
> Google GroupesA Nantes FP.
> > > > > Cette discussion peut A-atre lue sur le Web A l'adresse
> https://groups.google.com/d/msg/nantes-fp/-/nKXgMejAM3wJ.
> > > > > Pour envoyer un message A ce groupe, adressez un e-mail
> A A nant...@googlegroups.com.
> > > > > Pour vous dA(c)sabonner de ce groupe, envoyez un e-mail A
> l'adresse nantes-fp+...@googlegroups.com.
> > > > > Pour plus d'options, consultez la page de ce groupeA :

> http://groups.google.com/group/nantes-fp?hl=fr
> > > > >
>
> -----BEGIN PGP SIGNATURE-----
> Version: GnuPG v2.0.19 (GNU/Linux)
>
> iQIcBAEBAgAGBQJQqmkrAAoJEGv+hjwmhK0JrBYQAJ2pwCIoWOliJDuSQfn34V7O
> u3kTIdGVKF0O2ODmlRtcfw4ZZchtg2JJN29H26PqqljYm8NaCYA4lnPFwqVPKvWd
> VG9zxDquZ4R5k7pfw/qwSoxwmqTBfWx/qwAIDGOFliu0VdBQe7beRL0/ItzlOLyc
> jOKMeSkkixUqmMLDSoaWumqitZ/xMyXDBJ8xeURoSb6b9XCFUbPp+7cD+PvMcN2V
> Nstku8cAma6fVtSJ1gSw7EZpP4iqHOu954qgDKB5S6g72OguwCn7GVibzUtmW0Ey
> Ds5cGkKPKAtL4sPGZGzaGOZBizRZ5Qhq9Vs7P+8nGLq+ksyXdV2tXBNzlKn+p4EG
> /Zhdd3t6SaotjDInlXpJQZv18i9fGQQwMDpP6gV9VcB5ckUROZJZC7CltzJ1RXa+
> AxFAthHFgILRGWJslrJ3S7X4FbApz+o0R2nAYuc6XNQXZeDiyitJEGGUDDfw2hXQ
> gOcplBxLFHVVtikaw3MNZbrjDrtMn52UBkTVdfOfqDBuaYs6EhmiJXsc4EdFqNRA
> 81J6u5P2uDHe6Utm4bQyuGVz+1njMi6zFHvhecppEexv/BzJ25MwLREysMOz7R7o
> y77Csg3Uw6v0ZQhZBnQGe5oqjrIU76QiqtnZzLQGuDXWRZCDcM+7xB4ZB2N13l65
> HFrcOrwH2h5eSatfjAYX
> =91KN
> -----END PGP SIGNATURE-----
> --

> Vous recevez ce message, car vous A-ates abonnA(c) au groupe Google
> GroupesA Nantes FP.
> Pour envoyer un message A ce groupe, adressez un e-mail
> A A nant...@googlegroups.com.
> Pour vous dA(c)sabonner de ce groupe, envoyez un e-mail A l'adresse
> nantes-fp+...@googlegroups.com.
> Pour plus d'options, consultez la page de ce groupeA :
> http://groups.google.com/group/nantes-fp?hl=fr
>
> --
> CA(c)dric
>
> --
> Vous recevez ce message, car vous A-ates abonnA(c) au groupe Google
> GroupesA Nantes FP.
> Pour envoyer un message A ce groupe, adressez un e-mail
> A A nant...@googlegroups.com.
> Pour vous dA(c)sabonner de ce groupe, envoyez un e-mail A l'adresse
> nantes-fp+...@googlegroups.com.
> Pour plus d'options, consultez la page de ce groupeA :

> http://groups.google.com/group/nantes-fp?hl=fr
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.19 (GNU/Linux)

iQIcBAEBAgAGBQJQqznZAAoJEGv+hjwmhK0JelEP/iLFepiH5YpCf4DCkj7YXoHF
hGGU/pk+SbHOsWh0IIAI7E2lANGjo9LIW9iUmGaaEoOQDaKrGMRs0gTu43aJt2Zq
HVkLLbMISxrEZvMsw3uHjFYMWgWtmDwj4+vkqKUKCzulDNKcr06iJGkxIJ8YRQNq
untMHCFj+m32OiEbjBMgBd0Br69ttWabFY+HbyrkkVnINf6FZSZiXPZKZCLexg13
y45PQ9zKSRjqTjRcWlrUGX93zcHagqoDp+4O8BtoRkNQuviW6mP602aQfS6qJwZw
zVr1EWXLfxK+wW3lsbICpgiUSGSN+L8cbhQ+XpBSYRhbzYuVqf7D8GHB7x4UE5cC
DGJYIJghXxR86+Jq9qVAxMTIm73h7sR4Y0V3e812eDyOBCOF3XjGJMVcr1oaZN1c
tA9tanqBl8X69oMKj+rOosakPpUkcEs9Uo/a77fJsfPa7aDb0ui0CvlREcj+4DeH
RNdC//RfA/rNbBh/DCFe36wxM2a8C74lRmfMGJY5zF2QGRkuWn1aXeU9zIBGmfQo
dX7DrpHe2RuMA4sBpAnR1jRcZrzpQ9wljD7IB79eNPcMlokqojfRZOx79lEnaj6Q
W2exIeeQb6CLNZ4o+3lnfWk3CBqb9NMftX6CTiy2lzNWYO5XPyi3ubZ/BKWsiOPv
enHvIZrt1fIdKNizIp10
=vX7K
-----END PGP SIGNATURE-----

[Clément Delafargue]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

D'après le site de la cantine, une douzaine de places (ce n'est pas une salle de
conf, mais un espace de coworking). Pour info, la salle de conférence
"habituelle" permet d'accueillir 20 personnes en mode atelier.

Clément.

Pierre-Alexandre Voye wrote:
> Ya une limite en taille pour la salle ? C'est pour la news Linuxfr..
>

> Le 19 novembre 2012 17:53, ClA(c)ment Delafargue <cle...@delafargue.name>
> a A(c)crit :
>
> J'ai eu Magali, elle nous a rA(c)servA(c) le crA(c)neau et mis AS:a dans

> l'agenda de la
> cantine.
>

> On n'aura pas de vidA(c)oproj mais un A(c)cran, AS:a devrait suffire.
>
> ClA(c)ment

> ClA(c)ment Delafargue wrote:
> > J'ai eu Magali, la salle habituelle n'est *a priori* pas dispo, mais
> le nouvel

> > espace de coworking devrait l'A-atre. Par contre il n'y a pas de
> vidA(c)oproj lA bas.
> >
> > ClA(c)ment
> >
> > ClA(c)ment Delafargue wrote:

> > > A*a a l'air d'aller A tout le monde, donc oui.
> > > J'envoie un email A Magali DQP.
> > >
> > > ClA(c)ment

> > > Jonathan Winandy wrote:
> > > > C'est bon pour le mardi 27 nov ?
> > > >
> > > > Jon
> > > >
> > > > Le vendredi 16 novembre 2012 15:02:10 UTC+1, Clement Delafargue a

> A(c)crit :
> > > > >
> > > > > Ok. J'envoie l'email en fin d'aprA"m, histoire d'attendre
> d'autres rA(c)ponses.
> > > > >
> > > > > Cordialement,
> > > > > ClA(c)ment Delafargue
> > > > > cle...@delafargue.name <javascript:>
> > > > > http://www.eklaweb.com
> > > > >
> > > > > PGP Fingerprint : 5311 A6C4 8416 5378 3019 A B977 FFB4 9299 EAE0

> ED53
> > > > >
> > > > >
> > > > > 2012/11/16 Maxime Folschette <maxime.f...@gmail.com
> <javascript:>>
> > > > >
> > > > >> Salut,
> > > > >>
> > > > >> Ce n'est pas la date qui m'arrange le plus, mais comme l'agenda
> de la

> > > > >> Cantine doit A-atre plutA't bien chargA(c), je prends.

> > > > >> En plus c'est un mardi, ce qui pourra arranger plus de monde.
> > > > >>
> > > > >> Maxime
> > > > >>
> > > > >>
> > > > >>
> > > > >> On Friday, November 16, 2012 2:08:52 PM UTC+1, Pierre-Alexandre
> Voye
> > > > >> wrote:
> > > > >>
> > > > >>> Ok pour moi
> > > > >>>
> > > > >>>
> > > > >>> Le 16 novembre 2012 14:04, Clement Delafargue
> <diva...@gmail.com> a

> > > > >>> A(c)crit :
> > > > >>>
> > > > >>> Hop,
> > > > >>>>
> > > > >>>> DA(c)solA(c) pour le silence radio, j'ai un peu eu la tA-ate

> sous l'eau ces
> > > > >>>> derniers temps.
> > > > >>>>
> > > > >>>> Je propose la date du 27 novembre qui est libre sur le
> calendrier de la
> > > > >>>> cantine.

> > > > >>>> Si cela va A tout le monde, je rA(c)serve auprA"s de la
> Cantine.
> > > > >>>>
> > > > >>>> Cheers,
> > > > >>>> ClA(c)ment
> > > > >>>>
> > > > >>>>

> > > > >>>> On Tuesday, October 30, 2012 8:45:10 AM UTC+1, Simon

> ThA(c)pot wrote:
> > > > >>>>>
> > > > >>>>> Bonjour,
> > > > >>>>>
> > > > >>>>> ca fait un certain temps que je suis la mailing list mais je

> > > > >>>>> n'interviens pas car hA(c)las, tous mes jeudis soirs sont
> pris (et qui plus
> > > > >>>>> est je n'ai pas un gros background thA(c)orique A faire

> partager, je code en
> > > > >>>>> python/js et je suis venu naturellement vers le paradigme
> fonctionnel qui

> > > > >>>>> semble trA"s convaincant).
> > > > >>>>> Je me mets sur le doodle mais A moins que ca ne se passe la

> semaine
> > > > >>>>> prochaine (ou je n'ai pas cours de ahem.. salsa !),

> > > > >>>>> je ne pourrai pas venir, A mon grand regret.

> > > > >>>>>
> > > > >>>>> En tout cas, joli sujet !
> > > > >>>>> Merci,
> > > > >>>>>
> > > > >>>>> Simon
> > > > >>>>>
> > > > >>>>> Le lundi 29 octobre 2012 21:28:44 UTC+1, Maxime Folschette a

> A(c)crit :
> > > > >>>>>>
> > > > >>>>>> Merci A tous pour votre enthousiasmea*-! Faire plusieurs
> sA(c)ances ne
> > > > >>>>>> sera pas un gros problA"me, AS:a permettra de mieux
> rA(c)partir le contenu.
> > > > >>>>>> Merci Pierre-Alexandre d'avoir relancA(c) le truc, et
> dA(c)solA(c) pour mon
> > > > >>>>>> temps de rA(c)ponse.
> > > > >>>>>>

> > > > >>>>>> Le mieux serait de savoir quand la cantine sera disponible,

> AS:a sera
> > > > >>>>>> peut-A-atre le facteur le plus limitant.

> > > > >>>>>> Personnellement, je suis pour le moment disponible tous les
> soirs de

> > > > >>>>>> semaine A partir du lundi 5 novembre (exception faite des

> vendredis soirs,
> > > > >>>>>> qui ne naturellement pas partie de la semaine).
> > > > >>>>>>

> > > > >>>>>> Je pense finalement faire trois sA(c)ances puisque tout le
> monde semble

> > > > >>>>>> intA(c)ressA(c) par chaque sujet.
> > > > >>>>>>
> > > > >>>>>> La premiA"re sA(c)ance sera axA(c)e sur la prA(c)sentation
> de Coqa*-:

> > > > >>>>>> gA(c)nA(c)ralitA(c)s, utilisation, et un petit lot

> d'exemples et de preuves
> > > > >>>>>> relativement simples pour comprendre le fonctionnement de

> la bA-ate. Au
> > > > >>>>>> niveau du format, je propose de faire une sA(c)ance un peu
> hybridea*-: le rythme

> > > > >>>>>> sera assez lent pour que tout le monde puisse

> rA(c)A(c)crire, tester et rA(c)flA(c)chir
> > > > >>>>>> aux exemples proposA(c)s sur sa machine personnelle, mais
> AS:a se sera pas une
> > > > >>>>>> obligation pour pouvoir profiter de la sA(c)ance car les
> exemples seront

> > > > >>>>>> projetA(c)s et testA(c)s en direct. Je vous toucherai un

> mot sur la mise ne place
> > > > >>>>>> d'un environnement Coq prochainement. Enfin, pour les

> intA(c)ressA(c)s qui ne
> > > > >>>>>> pourront pas A-atre lA , je pourrai laisser mes notes en
> ligne.
> > > > >>>>>>
> > > > >>>>>> Seul problA"mea*-: je n'ai plus d'ordinateur portable, il
> faudrait donc
> > > > >>>>>> qu'on me prA-ate une machine le temps du sA(c)minaire, sur

> laquelle je sois en
> > > > >>>>>> mesure d'installer mon environnement Coq.
> > > > >>>>>>

> > > > >>>>>> A* voir donc quand la Cantine serait disponible.
> > > > >>>>>> Je continue A bosser sur le cours en attendant.

> > > > >>>>>>
> > > > >>>>>> Maxime
> > > > >>>>>>
> > > > >>>>>>
> > > > >>>>>> Le lundi 22 octobre 2012 16:18:40 UTC+2, Pierre-Alexandre
> Voye a

> > > > >>>>>> A(c)crit :
> > > > >>>>>>>
> > > > >>>>>>> J'ai crA(c)A(c) un doodle avec une date bidon pour savoir
> qui veut
> > > > >>>>>>> participer.
> > > > >>>>>>>

> > > > >>>>>>> On va essayer d'avoir la possibilitA(c) de faire AS:a A
> la cantine, ce
> > > > >>>>>>> qui rA(c)duira les possibilitA(c)s quand aux dates.
> > > > >>>>>>>
> > > > >>>>>>> Maxime, quand serais-tu plutA't disponible ?

> > > > >>>>>>> De mA-ame pour les autres ?

> > > > >>>>>>>
> > > > >>>>>>> Le doodle :
> > > > >>>>>>>
> http://www.doodle.com/**wz7fcn6f**b8b8uqm2<http://www.doodle.com/wz7fcn6fb8b8uqm2>
> > > > >>>>>>>
> > > > >>>>>>> Le 12 octobre 2012 10:37, Clement Delafargue
> <cle...@delafargue.name

> > > > >>>>>>> > a A(c)crit :
> > > > >>>>>>>
> > > > >>>>>>>> Pareil, pour moi, super intA(c)ressA(c) par 2a et 2b.
> > > > >>>>>>>>
> > > > >>>>>>>> Cordialement,
> > > > >>>>>>>> ClA(c)ment Delafargue
> > > > >>>>>>>> cle...@delafargue.name
> > > > >>>>>>>> http://www.eklaweb.com
> > > > >>>>>>>>
> > > > >>>>>>>> PGP Fingerprint : 5311 A6C4 8416 5378 3019 A B977 FFB4

> 9299 EAE0 ED53
> > > > >>>>>>>>
> > > > >>>>>>>>
> > > > >>>>>>>> Le 12 octobre 2012 08:54, Mogzor <mog...@gmail.com> a

> A(c)crit :
> > > > >>>>>>>> > 2a et 2b aussi pour ma part, en deux sA(c)ances,

> plutA't aprA"s les

> > > > >>>>>>>> > vacances de toussaint si y a moyen pour moi.
> > > > >>>>>>>> >

> > > > >>>>>>>> > Et super comme idA(c)e de conf :)

> > > > >>>>>>>> >
> > > > >>>>>>>> > Hugo
> > > > >>>>>>>> >
> > > > >>>>>>>> > 2012/10/11 Nicolas Rey <nicolas...@gmail.com>:

> > > > >>>>>>>> >> Peu de chance que je sois encore A Nantes lorsque

> AS:a aura lieu,
> > > > >>>>>>>> mais 2a et
> > > > >>>>>>>> >> 2b m'intA(c)resseraient bien !

> > > > >>>>>>>> >>
> > > > >>>>>>>> >> Nicolas REY
> > > > >>>>>>>> >>
> > > > >>>>>>>> >>
> > > > >>>>>>>> >> Le 11 octobre 2012 17:12, Albert

> <alber...@see4sys.com> a A(c)crit
> > > > >>>>>>>> :
> > > > >>>>>>>> >>
> > > > >>>>>>>> >>> Bonjour,
> > > > >>>>>>>> >>>
> > > > >>>>>>>> >>> Effectivement, c'est intA(c)ressant.
> > > > >>>>>>>> >>> 2a et 2b tant qu'A faire et 2 sA(c)ances c'est peut
> A-atre mA-ame
> > > > >>>>>>>> prA(c)fA(c)rable pour
> > > > >>>>>>>> >>> 'digA(c)rer' les diffA(c)rents A(c)lA(c)ments.
> > > > >>>>>>>> >>>

> > > > >>>>>>>> >>> Ensuite, si possible pas avant fin octobre me
> concernant (w44).
> > > > >>>>>>>> >>>
> > > > >>>>>>>> >>> Cdt,
> > > > >>>>>>>> >>>
> > > > >>>>>>>> >>> Albert.
> > > > >>>>>>>> >>>
> > > > >>>>>>>> >>> ______________________________****__
> > > > >>>>>>>> >>> De: "Pierre-Alexandre Voye" <ontol...@gmail.com>

> > > > >>>>>>>> >>> A*: nant...@googlegroups.com
> > > > >>>>>>>> >>> EnvoyA(c): Jeudi 11 Octobre 2012 16:55:38
> > > > >>>>>>>> >>> Objet: Re: Proposition pour la prochaine sA(c)ance :

> l'assistant
> > > > >>>>>>>> de preuves
> > > > >>>>>>>> >>> formelles Coq
> > > > >>>>>>>> >>>
> > > > >>>>>>>> >>>

> > > > >>>>>>>> >>> Moi AS:a me tente parce que AS:a fait 10 ans que je
> tourne autour
> > > > >>>>>>>> sans jamais
> > > > >>>>>>>> >>> m'y mettre sA(c)rieusement.

> > > > >>>>>>>> >>> C'est passionnant et c'est important de sensibiliser

> les gens A
> > > > >>>>>>>> AS:a.

> > > > >>>>>>>> >>> AprA"s je pense qu'il va falloir y aller tout le

> monde, sinon ya
> > > > >>>>>>>> que 3
> > > > >>>>>>>> >>> personnes qui vont comprendre
> > > > >>>>>>>> >>>

> > > > >>>>>>>> >>> On peut mA-ame tenter la news linuxfr car le sujet

> est clairement
> > > > >>>>>>>> ardu et
> > > > >>>>>>>> >>> seul les courageux viendront ;-)
> > > > >>>>>>>> >>>
> > > > >>>>>>>> >>> Le 11 octobre 2012 16:48, Maxime Folschette <
> > > > >>>>>>>> maxime.f...@gmail.com>

> > > > >>>>>>>> >>> a A(c)crit :
> > > > >>>>>>>> >>>>
> > > > >>>>>>>> >>>> Bonjour A tous,
> > > > >>>>>>>> >>>>
> > > > >>>>>>>> >>>> Pour la prochaine sA(c)ance du Nantes FP Group et
> aprA"s
> > > > >>>>>>>> discussion avec

> > > > >>>>>>>> >>>> ClA(c)ment, je vous propose une sA(c)ance autour de

> Coq [1], qui est
> > > > >>>>>>>> un assistant
> > > > >>>>>>>> >>>> de preuves formelles.

> > > > >>>>>>>> >>>> Certains se demanderont peut-A-atre A premiA"re vue

> quel rapport
> > > > >>>>>>>> cela pourra
> > > > >>>>>>>> >>>> avoir avec la programmation fonctionnelle, mais le
> lien est en

> > > > >>>>>>>> rA(c)alitA(c) trA"s
> > > > >>>>>>>> >>>> A(c)troit.
> > > > >>>>>>>> >>>>
> > > > >>>>>>>> >>>> En quelques mots, Coq permet de dA(c)finir des
> objets

> > > > >>>>>>>> mathA(c)matiques A l'aide

> > > > >>>>>>>> >>>> du langage Gallina (qui est purement fonctionnel).
> Ces objets
> > > > >>>>>>>> peuvent
> > > > >>>>>>>> >>>> globalement prendre la forme de types, fonctions ou
> > > > >>>>>>>> propositions

> > > > >>>>>>>> >>>> mathA(c)matiques. Dans un deuxiA"me temps, Coq

> permet, A l'aide
> > > > >>>>>>>> d'un
> > > > >>>>>>>> >>>> environnement de dA(c)monstration bien fourni,

> d'effectuer la
> > > > >>>>>>>> preuve des

> > > > >>>>>>>> >>>> diverses propositions que vous avez avancA(c)es.

> > > > >>>>>>>> >>>> Un exemple trA"s simple (et trA"s courant)

> d'utilisation de Coq,
> > > > >>>>>>>> qui sera

> > > > >>>>>>>> >>>> certainement le premier exemple de la sA(c)ance, est
> la
> > > > >>>>>>>> dA(c)finition de

> > > > >>>>>>>> >>>> l'ensemble des entiers naturels, puis la

> dA(c)finition de

> > > > >>>>>>>> l'addition sur ces
> > > > >>>>>>>> >>>> entiers. Par la suite, on pourra vouloir prouver
> sont la

> > > > >>>>>>>> commutativitA(c) et
> > > > >>>>>>>> >>>> l'associativitA(c) de cette opA(c)ration.

> > > > >>>>>>>> >>>> L'utilisation de Coq peut aller trA"s loin. On peut
> notamment
> > > > >>>>>>>> s'en servir
> > > > >>>>>>>> >>>> pour prouver des programmes impA(c)ratifs A l'aide

> de logique de
> > > > >>>>>>>> Hoare par

> > > > >>>>>>>> >>>> exemple [2]. Il a aussi permis la dA(c)monstration
> de certains
> > > > >>>>>>>> thA(c)orA"mes, donc

> > > > >>>>>>>> >>>> le plus cA(c)lA"bre est le thA(c)orA"me des quatre
> couleurs [3].
> > > > >>>>>>>> >>>>
> > > > >>>>>>>> >>>> Son lien A(c)troit avec la programmation

> fonctionnelle, outre le
> > > > >>>>>>>> langage
> > > > >>>>>>>> >>>> Gallina, se situe au niveau d'une notion qu'on
> appelle
> > > > >>>>>>>> l'isomorphisme de

> > > > >>>>>>>> >>>> Curry-Howard, qui stipule la prA(c)sence d'une
> correspondance
> > > > >>>>>>>> entre preuve et
> > > > >>>>>>>> >>>> fonction mathA(c)matique. Cette correspondance est

> un peu
> > > > >>>>>>>> subtile, mais je vous

> > > > >>>>>>>> >>>> propose de la dA(c)couvrir au terme de cette
> sA(c)ance, ou d'une
> > > > >>>>>>>> seconde sA(c)ance si
> > > > >>>>>>>> >>>> nA(c)cessaire.
> > > > >>>>>>>> >>>>

> > > > >>>>>>>> >>>> Je vous propose donc le programme suivant (assez

> consA(c)quent)
> > > > >>>>>>>> autour de
> > > > >>>>>>>> >>>> Coqa*-:
> > > > >>>>>>>> >>>> 1) Introduction A Coq et au langage de description
> Gallinaa*-:
> > > > >>>>>>>> dA(c)finitions

> > > > >>>>>>>> >>>> basiques d'objets mathA(c)matiques et utilisation de
> > > > >>>>>>>> l'environnement de

> > > > >>>>>>>> >>>> preuvesa*-;
> > > > >>>>>>>> >>>> 2a) Preuve de programmes impA(c)ratifsa*-: aprA"s
> avoir dA(c)fini la
> > > > >>>>>>>> grammaire et

> > > > >>>>>>>> >>>> la sA(c)mantique d'un langage impA(c)ratif simple,

> il devient
> > > > >>>>>>>> possible de prouver
> > > > >>>>>>>> >>>> que celui-ci observe le comportement

> dA(c)sirA(c)a*-;
> > > > >>>>>>>> >>>> 2b) PrA(c)sentation de l'isomorphisme de

> Curry-Howarda*-: il est

> > > > >>>>>>>> possible de
> > > > >>>>>>>> >>>> se passer de l'environnement de preuves de Coq et

> d'A(c)crire les
> > > > >>>>>>>> preuves de

> > > > >>>>>>>> >>>> thA(c)orA"mes sous forme de fonctions, leur
> correction A(c)tant
> > > > >>>>>>>> assurA(c)e grA-c-ce au

> > > > >>>>>>>> >>>> typage fort de Gallina.
> > > > >>>>>>>> >>>>
> > > > >>>>>>>> >>>> Ce programme se divise en deux branches (2a et 2b)
> qui ne sont
> > > > >>>>>>>> pas

> > > > >>>>>>>> >>>> antinomiques, mais qui auraient plutA't intA(c)rA-at
> A A-atre traitA(c)es
> > > > >>>>>>>> sA(c)parA(c)ment.

> > > > >>>>>>>> >>>> Je souhaiterais ainsi avoir un retour de votre part
> afin de

> > > > >>>>>>>> savoira*-:
> > > > >>>>>>>> >>>> a** d'une part si ce sujet vous intA(c)resse,
> > > > >>>>>>>> >>>> a** d'autre part quel aspect (parmi 2a et 2b) vous
> prA(c)fA(c)reriez
> > > > >>>>>>>> A(c)tudier
> > > > >>>>>>>> >>>> (A<<a*-les deuxa*-A>> A(c)tant une rA(c)ponse tout

> A fait acceptable).
> > > > >>>>>>>> >>>>
> > > > >>>>>>>> >>>> Il restera aussi A discuter de la charge d'une
> telle sA(c)ance

> > > > >>>>>>>> (il sera
> > > > >>>>>>>> >>>> possible de la diviser si le sujet semble trop
> complexe pour

> > > > >>>>>>>> A-atre traitA(c) en

> > > > >>>>>>>> >>>> une fois), et naturellement de la date.
> > > > >>>>>>>> >>>>

> > > > >>>>>>>> >>>> Ceux qui sont curieux A propos de Coq pourront
> consulter un
> > > > >>>>>>>> tutoriel [2]
> > > > >>>>>>>> >>>> et un livre [4] A son propos.
> > > > >>>>>>>> >>>>
> > > > >>>>>>>> >>>> En attendant votre rA(c)ponse je vous souhaite une

> bonne fin de
> > > > >>>>>>>> semaine,
> > > > >>>>>>>> >>>>
> > > > >>>>>>>> >>>> Maxime
> > > > >>>>>>>> >>>>
> > > > >>>>>>>> >>>>
> > > > >>>>>>>> >>>> [1] http://coq.inria.fr/
> > > > >>>>>>>> >>>> [2]
> http://www.cis.upenn.edu/~**bcpi**erce/sf/<http://www.cis.upenn.edu/~bcpierce/sf/>
> > > > >>>>>>>> >>>> [3] https://fr.wikipedia.org/wiki/****
> > > > >>>>>>>>
> Th%C3%A9or%C3%A8me_des_quatre_****couleurs<https://fr.wikipedia.org/wiki/Th%C3%A9or%C3%A8me_des_quatre_couleurs>
> > > > >>>>>>>> >>>> [4]
> http://www.labri.fr/perso/**cast**eran/CoqArt/index.html<http://www.labri.fr/perso/casteran/CoqArt/index.html>
> > > > >>>>>>>> >>>>
> > > > >>>>>>>> >>>> --

> > > > >>>>>>>> >>>> Vous recevez ce message, car vous A-ates abonnA(c)

> au groupe Google
> > > > >>>>>>>> Groupes
> > > > >>>>>>>> >>>> Nantes FP.

> > > > >>>>>>>> >>>> Cette discussion peut A-atre lue sur le Web A

> l'adresse
> > > > >>>>>>>> >>>>
> https://groups.google.com/d/**ms**g/nantes-fp/-/4JyU9GutumAJ<https://groups.google.com/d/msg/nantes-fp/-/4JyU9GutumAJ>
> > > > >>>>>>>> .

> > > > >>>>>>>> >>>> Pour envoyer un message A ce groupe, adressez un
> e-mail A
> > > > >>>>>>>> >>>> nant...@googlegroups.com.

> > > > >>>>>>>> >>>> Pour vous dA(c)sabonner de ce groupe, envoyez un
> e-mail A

> > > > >>>>>>>> l'adresse
> > > > >>>>>>>> >>>> nantes-fp+...@googlegroups.com****.
> > > > >>>>>>>> >>>> Pour plus d'options, consultez la page de ce groupe
> :
> > > > >>>>>>>> >>>>
> http://groups.google.com/**group**/nantes-fp?hl=fr<http://groups.google.com/group/nantes-fp?hl=fr>
> > > > >>>>>>>> >>>
> > > > >>>>>>>> >>>
> > > > >>>>>>>> >>>
> > > > >>>>>>>> >>>
> > > > >>>>>>>> >>> --
> > > > >>>>>>>> >>> ---------------------
> > > > >>>>>>>> >>>
> https://twitter.com/#!/**ontolog**iae/<https://twitter.com/#!/ontologiae/>
> > > > >>>>>>>> >>>
> http://linuxfr.org/users/**monta**igne<http://linuxfr.org/users/montaigne>
> > > > >>>>>>>> >>>
> > > > >>>>>>>> >>> --

> > > > >>>>>>>> >>> Vous recevez ce message, car vous A-ates abonnA(c) au

> groupe Google
> > > > >>>>>>>> Groupes
> > > > >>>>>>>> >>> Nantes FP.

> > > > >>>>>>>> >>> Pour envoyer un message A ce groupe, adressez un
> e-mail A
> > > > >>>>>>>> >>> nant...@googlegroups.com.

> > > > >>>>>>>> >>> Pour vous dA(c)sabonner de ce groupe, envoyez un
> e-mail A l'adresse

> > > > >>>>>>>> >>> nantes-fp+...@googlegroups.com****.
> > > > >>>>>>>> >>> Pour plus d'options, consultez la page de ce groupe :
> > > > >>>>>>>> >>>
> http://groups.google.com/**group**/nantes-fp?hl=fr<http://groups.google.com/group/nantes-fp?hl=fr>
> > > > >>>>>>>> >>>
> > > > >>>>>>>> >>> --

> > > > >>>>>>>> >>> Vous recevez ce message, car vous A-ates abonnA(c) au

> groupe Google
> > > > >>>>>>>> Groupes
> > > > >>>>>>>> >>> Nantes FP.

> > > > >>>>>>>> >>> Pour envoyer un message A ce groupe, adressez un
> e-mail A
> > > > >>>>>>>> >>> nant...@googlegroups.com.

> > > > >>>>>>>> >>> Pour vous dA(c)sabonner de ce groupe, envoyez un
> e-mail A l'adresse

> > > > >>>>>>>> >>> nantes-fp+...@googlegroups.com****.
> > > > >>>>>>>> >>> Pour plus d'options, consultez la page de ce groupe :
> > > > >>>>>>>> >>>
> http://groups.google.com/**group**/nantes-fp?hl=fr<http://groups.google.com/group/nantes-fp?hl=fr>
> > > > >>>>>>>> >>
> > > > >>>>>>>> >>
> > > > >>>>>>>> >> --

> > > > >>>>>>>> >> Vous recevez ce message, car vous A-ates abonnA(c) au

> groupe Google
> > > > >>>>>>>> Groupes
> > > > >>>>>>>> >> Nantes FP.

> > > > >>>>>>>> >> Pour envoyer un message A ce groupe, adressez un
> e-mail A
> > > > >>>>>>>> >> nant...@googlegroups.com.

> > > > >>>>>>>> >> Pour vous dA(c)sabonner de ce groupe, envoyez un
> e-mail A l'adresse

> > > > >>>>>>>> >> nantes-fp+...@googlegroups.com****.
> > > > >>>>>>>> >> Pour plus d'options, consultez la page de ce groupe :
> > > > >>>>>>>> >>
> http://groups.google.com/**group**/nantes-fp?hl=fr<http://groups.google.com/group/nantes-fp?hl=fr>
> > > > >>>>>>>> >
> > > > >>>>>>>> > --

> > > > >>>>>>>> > Vous recevez ce message, car vous A-ates abonnA(c) au

> groupe Google
> > > > >>>>>>>> Groupes Nantes FP.

> > > > >>>>>>>> > Pour envoyer un message A ce groupe, adressez un
> e-mail A
> > > > >>>>>>>> nant...@googlegroups.com.

> > > > >>>>>>>> > Pour vous dA(c)sabonner de ce groupe, envoyez un e-mail
> A l'adresse

> > > > >>>>>>>> nantes-fp+...@googlegroups.com****.
> > > > >>>>>>>> > Pour plus d'options, consultez la page de ce groupe :
> > > > >>>>>>>>
> http://groups.google.com/**group**/nantes-fp?hl=fr<http://groups.google.com/group/nantes-fp?hl=fr>
> > > > >>>>>>>> >
> > > > >>>>>>>>
> > > > >>>>>>>> --

> > > > >>>>>>>> Vous recevez ce message, car vous A-ates abonnA(c) au

> groupe Google
> > > > >>>>>>>> Groupes Nantes FP.

> > > > >>>>>>>> Pour envoyer un message A ce groupe, adressez un e-mail
> A
> > > > >>>>>>>> nant...@googlegroups.com.

> > > > >>>>>>>> Pour vous dA(c)sabonner de ce groupe, envoyez un e-mail
> A l'adresse

> > > > >>>>>>>> nantes-fp+...@googlegroups.com****.
> > > > >>>>>>>> Pour plus d'options, consultez la page de ce groupe :
> > > > >>>>>>>>
> http://groups.google.com/**group**/nantes-fp?hl=fr<http://groups.google.com/group/nantes-fp?hl=fr>
> > > > >>>>>>>>
> > > > >>>>>>>>
> > > > >>>>>>>
> > > > >>>>>>>
> > > > >>>>>>> --
> > > > >>>>>>> ---------------------
> > > > >>>>>>>
> https://twitter.com/#!/**ontolog**iae/<https://twitter.com/#%21/ontologiae/>
> > > > >>>>>>>
> http://linuxfr.org/users/**monta**igne<http://linuxfr.org/users/montaigne>
> > > > >>>>>>>

> > > > >>>>>>> A --
> > > > >>>> Vous recevez ce message, car vous A-ates abonnA(c) au groupe
> Google
> > > > >>>> Groupes Nantes FP.
> > > > >>>> Cette discussion peut A-atre lue sur le Web A l'adresse

> > > > >>>>
> https://groups.google.com/d/**msg/nantes-fp/-/IDdBVSChjlwJ<https://groups.google.com/d/msg/nantes-fp/-/IDdBVSChjlwJ>
> > > > >>>> .
> > > > >>>>

> > > > >>>> Pour envoyer un message A ce groupe, adressez un e-mail A
> > > > >>>> nant...@googlegroups.com.

> > > > >>>> Pour vous dA(c)sabonner de ce groupe, envoyez un e-mail A

> l'adresse
> > > > >>>> nantes-fp+...@**googlegroups.com.
> > > > >>>> Pour plus d'options, consultez la page de ce groupe :
> > > > >>>>
> http://groups.google.com/**group/nantes-fp?hl=fr<http://groups.google.com/group/nantes-fp?hl=fr>
> > > > >>>>
> > > > >>>
> > > > >>>
> > > > >>>
> > > > >>> --
> > > > >>> ---------------------
> > > > >>>
> https://twitter.com/#!/**ontologiae/<https://twitter.com/#%21/ontologiae/>
> > > > >>>
> http://linuxfr.org/users/**montaigne<http://linuxfr.org/users/montaigne>
> > > > >>>

> > > > >>> A --
> > > > >> Vous recevez ce message, car vous A-ates abonnA(c) au groupe
> Google
> > > > >> Groupes Nantes FP.
> > > > >> Cette discussion peut A-atre lue sur le Web A l'adresse
> > > > >> https://groups.google.com/d/msg/nantes-fp/-/7YPlZEkRrDQJ.
> > > > >>
> > > > >> Pour envoyer un message A ce groupe, adressez un e-mail A
> > > > >> nant...@googlegroups.com <javascript:>.
> > > > >> Pour vous dA(c)sabonner de ce groupe, envoyez un e-mail A

> l'adresse
> > > > >> nantes-fp+...@googlegroups.com <javascript:>.
> > > > >> Pour plus d'options, consultez la page de ce groupe :
> > > > >> http://groups.google.com/group/nantes-fp?hl=fr
> > > > >>
> > > > >
> > > > >
> > > >
> > > > --

> > > > Vous recevez ce message, car vous A-ates abonnA(c) au groupe

> Google GroupesA Nantes FP.
> > > > Cette discussion peut A-atre lue sur le Web A l'adresse
> https://groups.google.com/d/msg/nantes-fp/-/nKXgMejAM3wJ.

> > > > Pour envoyer un message A ce groupe, adressez un e-mail
> A A nant...@googlegroups.com.

> > > > Pour vous dA(c)sabonner de ce groupe, envoyez un e-mail A
> l'adresse nantes-fp+...@googlegroups.com.
> > > > Pour plus d'options, consultez la page de ce groupeA :

> http://groups.google.com/group/nantes-fp?hl=fr
> > > >
>
> --
> ---------------------
> https://twitter.com/#!/ontologiae/
> http://linuxfr.org/users/montaigne
>

> --

> Vous recevez ce message, car vous A-ates abonnA(c) au groupe Google

> GroupesA Nantes FP.

> Pour envoyer un message A ce groupe, adressez un e-mail
> A A nant...@googlegroups.com.

> Pour vous dA(c)sabonner de ce groupe, envoyez un e-mail A l'adresse
> nantes-fp+...@googlegroups.com.

> Pour plus d'options, consultez la page de ce groupeA :
> http://groups.google.com/group/nantes-fp?hl=fr
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.19 (GNU/Linux)

iQIcBAEBAgAGBQJQqzsCAAoJEGv+hjwmhK0J+OIP+weBChE1biRYxO+B3IUce4if
d03Q0vYPMJvpluYVqQ1ADd58Oliuccp6vCOddMn9e03r/pb5bczgsfKRas7SYTJ4
3mIiInq29geiP4r47I5iFo7bEde1JA1AKCIKJ5pT1Ux3cvycMPaPCGObOnDlQzLn
yJ+yUwISi+Dlfrzz8497F5LwcT1GI8mYc7r5EkZmP0u9T37v8zOGCu5qjcBIfcUa
LvrojuNQcqevGX+VAMeG8udTyOUFduqw0ezZ13t2CGrFa+JacITxxhN3ZxzZ6qGf
VcUyqRLKHNu2N5ggpAtZcZTCfKP9qJRBMfb4YJt5Olmmp5H/xOzrQ1jjQ3xz+eV1
dhd3Jm030906AXGmHAmJMDGW+iCSpBqZMwTKffXnUNHAH4JjHlSPEOaxDFhcQuC8
hlRBQ0faU/IB/LWRLDEMbLREHe4RuJG8ILm9+Dg7hTQiCEGKTcFBKBcGTKzpqBfM
mch8Pd4ZTzKJZyEZ2Up+WYMEjXuV5d8B0rxaG8sfkKchu9nGmoh8NHUNhoEfcvep
jXgakAFxkbHxRNAE4KnlQ3AiMgo1LXkCzrNUeYpCPsI0AcjjQljGHDPTZu0sGCmX
euI+P4OGdMgRvJZDh+0JufWqwzPA5lVvlPZIVumdYs1G5xyW2naaHMkM0QUjSXh8
Kcv7oF3YcIwx4az4JUCp
=/fsg
-----END PGP SIGNATURE-----

[Maxime Folschette]

Je pense que l'introduction de cette première séance sera davantage axée sur les notions mathématiques nécessaires comprendre le fonctionnement et l'utilité de Coq. Je toucherai peut-être un mot de ce dont il est question dans l'article, mais je ne m'étendrai pas davantage dessus :
— parce qu'il s'agira avant tout d'une séance orientée maths et je veux m'assurer d'offrir les bonnes bases de maths et de Coq à tout le monde avant de parler de notions plus complexes,
— parce que l'isomorphisme de Curry-Howard sera l'objet de la dernière séance (qui pourra alors dépasser le cadre de Coq).

Patience, donc !

Maxime

[Clément Delafargue]

Croyez-le ou non, mais j'ai mis le site à jour.

http://nantes-fp.github.com/2012/11/20/coq-part1/

Maxime Folschette wrote:
> Je pense que l'introduction de cette première séance sera davantage axée
> sur les notions mathématiques nécessaires comprendre le fonctionnement et
> l'utilité de Coq. Je toucherai peut-être un mot de ce dont il est question
> dans l'article, mais je ne m'étendrai pas davantage dessus :
> — parce qu'il s'agira avant tout d'une séance orientée maths et je veux
> m'assurer d'offrir les bonnes bases de maths et de Coq à tout le monde
> avant de parler de notions plus complexes,
> — parce que l'isomorphisme de Curry-Howard sera l'objet de la dernière
> séance (qui pourra alors dépasser le cadre de Coq).
>
> Patience, donc !
>
> Maxime
>
>
> On Monday, November 19, 2012 9:01:09 PM UTC+1, Cédric Pineau wrote:
> >
> >
> > Je ne sais pas si c'est prévu, mais une petite introduction permettant de
> > placer Coq au sein du mouvement plus global que je crois deviner au travers
> > de cet article par exemple serait vraiment top :-)
> >
> >
> > http://www.dzone.com/links/r/unifying_programming_and_math_the_dependent_type.html
> >
> > Cédric
> >
> >
> >

> > Le 19 novembre 2012 18:15, Clément Delafargue <cle...@delafargue.name<javascript:>

> >> -----BEGIN PGP SIGNATURE-----
> >> Version: GnuPG v2.0.19 (GNU/Linux)
> >>
> >> iQIcBAEBAgAGBQJQqmkrAAoJEGv+hjwmhK0JrBYQAJ2pwCIoWOliJDuSQfn34V7O
> >> u3kTIdGVKF0O2ODmlRtcfw4ZZchtg2JJN29H26PqqljYm8NaCYA4lnPFwqVPKvWd
> >> VG9zxDquZ4R5k7pfw/qwSoxwmqTBfWx/qwAIDGOFliu0VdBQe7beRL0/ItzlOLyc
> >> jOKMeSkkixUqmMLDSoaWumqitZ/xMyXDBJ8xeURoSb6b9XCFUbPp+7cD+PvMcN2V
> >> Nstku8cAma6fVtSJ1gSw7EZpP4iqHOu954qgDKB5S6g72OguwCn7GVibzUtmW0Ey
> >> Ds5cGkKPKAtL4sPGZGzaGOZBizRZ5Qhq9Vs7P+8nGLq+ksyXdV2tXBNzlKn+p4EG
> >> /Zhdd3t6SaotjDInlXpJQZv18i9fGQQwMDpP6gV9VcB5ckUROZJZC7CltzJ1RXa+
> >> AxFAthHFgILRGWJslrJ3S7X4FbApz+o0R2nAYuc6XNQXZeDiyitJEGGUDDfw2hXQ
> >> gOcplBxLFHVVtikaw3MNZbrjDrtMn52UBkTVdfOfqDBuaYs6EhmiJXsc4EdFqNRA
> >> 81J6u5P2uDHe6Utm4bQyuGVz+1njMi6zFHvhecppEexv/BzJ25MwLREysMOz7R7o
> >> y77Csg3Uw6v0ZQhZBnQGe5oqjrIU76QiqtnZzLQGuDXWRZCDcM+7xB4ZB2N13l65
> >> HFrcOrwH2h5eSatfjAYX
> >> =91KN
> >> -----END PGP SIGNATURE-----
> >>
> >> --
> >> Vous recevez ce message, car vous êtes abonné au groupe Google
> >> Groupes Nantes FP.
> >> Pour envoyer un message à ce groupe, adressez un e-mail à

> >> nant...@googlegroups.com <javascript:>.
> >> Pour vous désabonner de ce groupe, envoyez un e-mail à l'adresse
> >> nantes-fp+...@googlegroups.com <javascript:>.
> >> Pour plus d'options, consultez la page de ce groupe :
> >> http://groups.google.com/group/nantes-fp?hl=fr
> >>
> >>
> >
> >
> > --

> > Cédric

> >
> >
>
> --
> Vous recevez ce message, car vous êtes abonné au groupe Google Groupes Nantes FP.

> Cette discussion peut être lue sur le Web à l'adresse https://groups.google.com/d/msg/nantes-fp/-/9VckXUK6mQMJ.

[Maxime Folschette]

Bonjour à tous,

Le séminaire approche. Afin que la séance soit la plus dynamique possible, toutes mes explications sur Coq seront suivies d'une démonstration en direct. Je projetterai donc du code Coq qui sera complété (et vérifié) sous vos yeux. Cela vous permettra de participer, et ceux qui le souhaitent pourront reprendre le code et le tester eux-mêmes en même temps. Si le temps le permet, il pourra aussi être question de résoudre quelques exercices pour vous faire travailler les méninges.

Pour cela, je vous encourage à installer Coq sur votre machine personnelle. Vous le trouverez à [1] ou via le paquer “coq”, dans vos paquets officiels pour certaines distributions Linux.
Il vous faudra aussi un IDE pour pouvoir utiliser Coq dans les meilleurs conditions. Deux possibilités alors :
— CoqIDE, qui est l'IDE officiel de Coq ; vous le trouverez avec Coq, à [1] ou via le paquet “coqide”.
— Si vous ne parvenez pas à utiliser CoqIDE ou que vous préférez une alternative, vous pouvez utiliser le module ProofGeneral d'Emacs. Il nécessite Emacs mais a l'avantage d'être en conséquence un peu plus personnalisable. Vous le trouverez à [2] ou via le paquet “proofgeneral-coq”.
Pour les utilisateurs de ProofGeneral, je vous conseille d'ajouter les lignes qui suivent dans ~/.emacs (créez-le s'il n'existe pas) :

(eval-after-load "proof-script" '(progn
  (define-key proof-mode-map [(control n)] 'proof-assert-next-command-interactive)
  (define-key proof-mode-map [(control b)] 'proof-undo-last-successful-command)
  (define-key proof-mode-map [(control ,)] 'proof-goto-point)
  (define-key proof-mode-map [(control \;)] 'proof-retract-buffer) ))

Cela vous économisera des doigts.

N'hésitez pas à me faire part de vos problèmes d'installation si vous en rencontrez (même si je ne promets rien).

Je posterai naturellement le code final et le diaporama de la séance après coup.

À très bientôt !

Maxime

[1] http://coq.inria.fr/download
[2] http://proofgeneral.inf.ed.ac.uk/download

Le jeudi 11 octobre 2012 16:48:41 UTC+2, Maxime Folschette a écrit :

Bonjour à tous,

Pour la prochaine séance du Nantes FP Group et après discussion avec Clément, je vous propose une séance autour de Coq [1], qui est un assistant de preuves formelles.
Certains se demanderont peut-être à première vue quel rapport cela pourra avoir avec la programmation fonctionnelle, mais le lien est en réalité très étroit.

En quelques mots, Coq permet de définir des objets mathématiques à l'aide du langage Gallina (qui est purement fonctionnel). Ces objets peuvent globalement prendre la forme de types, fonctions ou propositions mathématiques. Dans un deuxième temps, Coq permet, à l'aide d'un environnement de démonstration bien fourni, d'effectuer la preuve des diverses propositions que vous avez avancées.
Un exemple très simple (et très courant) d'utilisation de Coq, qui sera certainement le premier exemple de la séance, est la définition de l'ensemble des entiers naturels, puis la définition de l'addition sur ces entiers. Par la suite, on pourra vouloir prouver sont la commutativité et l'associativité de cette opération.
L'utilisation de Coq peut aller très loin. On peut notamment s'en servir pour prouver des programmes impératifs à l'aide de logique de Hoare par exemple [2]. Il a aussi permis la démonstration de certains théorèmes, donc le plus célèbre est le théorème des quatre couleurs [3].

Son lien étroit avec la programmation fonctionnelle, outre le langage Gallina, se situe au niveau d'une notion qu'on appelle l'isomorphisme de Curry-Howard, qui stipule la présence d'une correspondance entre preuve et fonction mathématique. Cette correspondance est un peu subtile, mais je vous propose de la découvrir au terme de cette séance, ou d'une seconde séance si nécessaire.

Je vous propose donc le programme suivant (assez conséquent) autour de Coq :
1) Introduction à Coq et au langage de description Gallina : définitions basiques d'objets mathématiques et utilisation de l'environnement de preuves ;
2a) Preuve de programmes impératifs : après avoir défini la grammaire et la sémantique d'un langage impératif simple, il devient possible de prouver que celui-ci observe le comportement désiré ;
2b) Présentation de l'isomorphisme de Curry-Howard : il est possible de se passer de l'environnement de preuves de Coq et d'écrire les preuves de théorèmes sous forme de fonctions, leur correction étant assurée grâce au typage fort de Gallina.

Ce programme se divise en deux branches (2a et 2b) qui ne sont pas antinomiques, mais qui auraient plutôt intérêt à être traitées séparément. Je souhaiterais ainsi avoir un retour de votre part afin de savoir :
— d'une part si ce sujet vous intéresse,
— d'autre part quel aspect (parmi 2a et 2b) vous préféreriez étudier (« les deux » étant une réponse tout à fait acceptable).

Il restera aussi à discuter de la charge d'une telle séance (il sera possible de la diviser si le sujet semble trop complexe pour être traité en une fois), et naturellement de la date.

Ceux qui sont curieux à propos de Coq pourront consulter un tutoriel [2] et un livre [4] à son propos.

En attendant votre réponse je vous souhaite une bonne fin de semaine,

Maxime


[1] http://coq.inria.fr/

[Albert]

Bonjour,

N'ayant pas pu assister, j'aimerais savoir s'il y a des ressources utilisées pour la présentation disponibles en ligne quelque part ?

Merci,

Albert.

---

De: "Maxime Folschette" <maxime.f...@gmail.com>
À: nant...@googlegroups.com
Envoyé: Samedi 24 Novembre 2012 15:25:11

Objet: Re: Proposition pour la prochaine séance : l'assistant de preuves formelles Coq

--
Vous recevez ce message, car vous êtes abonné au groupe Google Groupes Nantes FP.

Cette discussion peut être lue sur le Web à l'adresse https://groups.google.com/d/msg/nantes-fp/-/sDZxD2J9JcgJ.

[Clement Delafargue]

Bonjour,

Tout est sur github :

https://github.com/nantes-fp/seance-coq

--
Envoyé depuis mon sanglier

[Albert]

Ah. Ok.
Désolé, j'avais loupé le truc.
Merci.

---

De: "Clement Delafargue" <diva...@gmail.com>
À: nant...@googlegroups.com
Envoyé: Jeudi 13 Décembre 2012 10:20:14

[Clement Delafargue]

Pas de problème :)

Il va d'ailleurs falloir penser à fixer les prochaines dates.

--
Envoyé depuis mon sanglier

[Albert]

Me concernant, ma contrainte sur les mardi demeure. En janvier, pas possible non plus le 7.

---

De: "Clement Delafargue" <diva...@gmail.com>
À: nant...@googlegroups.com

Envoyé: Jeudi 13 Décembre 2012 10:27:58

[Maxime Folschette]

Bonjour à tous,

Nous pouvons effectivement fixer la date du prochain rendez-vous. On peut envisager de changer de jour afin de permettre à de nouvelles personnes de venir.
Je n'ai à priori aucune contrainte hormis une impossibilité les 21 et 22 janvier.
Que dites-vous du mercredi 23 janvier par exemple ?

Concernant le contenu de la séance, il nous sera possible de revenir sur certains éléments qui avaient été vus lors de la première séance, et d'enrichir avec des points plus avancés. Cela permettrait aux nouveaux de pouvoir suivre tout en offrant du matériel neuf à ceux qui ont déjà pu participer.
Cependant, si vous préférez, nous pouvons directement nous attaquer à la preuve de programmes impératifs.

Dans l'attente de vos réponses,
Et bonne année à tous,

Maxime

[Rodolphe BELOUIN]

Bonjour à tous, et bonne année (pour faire original)

Le mercredi 23 me convient, personnellement.

À bientôt,

Rodolphe

2013/1/7 Maxime Folschette <maxime.f...@gmail.com>

Cette discussion peut être lue sur le Web à l'adresse https://groups.google.com/d/msg/nantes-fp/-/R6eD8j0tObEJ.

[Albert]

Bonjour,

Rien à changer au mail précédent : bonne année et ok me concernant pour le 23 :D

Albert.

---

De: "Rodolphe BELOUIN" <rodolphe...@gmail.com>
À: nant...@googlegroups.com
Cc: "albert pais" <alber...@see4sys.com>
Envoyé: Lundi 7 Janvier 2013 16:03:49

[Maxime Folschette]

Bonjour à tous,

Étant donné qu'il n'y a pas eu beaucoup de réponses et que le temps manque pour certains points d'organisation, je vous propose de repousser la prochaine réunion du séminaire.
Je vous propose une des deux dates suivantes :
— mercredi 30 janvier
— mercredi 6 février
Merci de donner vos préférences entre ces deux dates, ou d'en proposer d'autres si celles-ci ne vous convenaient pas.

Pour rappel, lors de cette prochaine séance, je vous propose de revoir et approfondir les notions déjà vues lors de la première séance, si cela convient à tout le monde.

Désolé pour ce report, j'espère qu'il permettra de contenter un maximum de monde.

Maxime

[Cédric Pineau]

 Je ne peux pas le 30, donc plutôt partant pour le 6 pour ma part !

--
Cédric

[Mogzor]

ok pour le 6

2013/1/17 Cédric Pineau <cedric...@gmail.com>:

>
> Je ne peux pas le 30, donc plutôt partant pour le 6 pour ma part !
>
> --
> Cédric
>

[Albert]

Bonjour,

Idem pour moi : pas de pb pour le 6.

Albert.

----- Mail original -----
De: "Mogzor" <mog...@gmail.com>
À: nant...@googlegroups.com
Envoyé: Jeudi 17 Janvier 2013 15:47:34

Objet: Re: Proposition pour la prochaine séance : l'assistant de preuves formelles Coq

[Maxime Folschette]

Bonjour à tous,

Encore une fois, la date du 6 février pose des problèmes.
Je vous propose donc une nouvelle date : le jeudi 14 février, 19 h 30 à la Cantine.

La séance devrait durer environ deux heures, et vous trouverez le programme ci-après.
J'espère que cela vous conviendra.

Maxime

~~~~

L'objectif de cette nouvelle séance sera de rappeler et d'approfondir les notions vues précédemment sur l'assistant de preuves formelles Coq [1].
Il sera question d'y voir ou revoir notamment les types paramétrés, les définitions récursives et les preuves par récurrence et par analyse de cas.
Plusieurs exercices, tirés du cours “Functional Programming Principles in Scala” de Martin Odersky sur Coursera [1], seront l'occasion d'appliquer ce qui a été vu au cours de ces deux séances à des exemples concrets.
Enfin, si le temps le permet, il sera possible de discuter de l'isomorphisme de Curry-Howard, que Coq utilise pour vérifier les preuves.

Autres références sur Coq : [3, 4].

[1] http://coq.inria.fr/
[2] https://www.coursera.org/course/progfun
[3] http://www.cis.upenn.edu/~bcpierce/sf/
[4] http://www.labri.fr/perso/casteran/CoqArt/index.html

[Rodolphe BELOUIN]

Cette date risque de poser problème aux petits romantiques :D

2013/1/23 Maxime Folschette <maxime.f...@gmail.com>

Cette discussion peut être lue sur le Web à l'adresse https://groups.google.com/d/msg/nantes-fp/-/Zup5nCNjOjoJ.

[Albert]

Salut,

Me concernant, j'ai pour l'instant un déplacement sur Paname prévu le 14. Je n'ai pas encore les détails, donc je ne sais pas si je serai là. Ceci dit, semaines 7 et 8 risquent de toute façon d'être un peu compliquées pour moi.

[Maxime Folschette]

Cette séance s'adresse à tous les amoureux de Coq ! La date est donc parfaitement choisie.

Maxime

[Rodolphe BELOUIN]

Je disais ça, mais pour moi c'est ok ;)

2013/1/23 Maxime Folschette <maxime.f...@gmail.com>

Cette discussion peut être lue sur le Web à l'adresse https://groups.google.com/d/msg/nantes-fp/-/uxIHGsfxA9UJ.

[Clement Delafargue]

Ça me va aussi.

Cordialement,
Clément Delafargue
cle...@delafargue.name
http://www.eklaweb.com

PGP Fingerprint : 5311 A6C4 8416 5378 3019 B977 FFB4 9299 EAE0 ED53

2013/1/23 Rodolphe BELOUIN <rodolphe...@gmail.com>:

[Pierre-Alexandre Voye]

ok pour moi aussi

[Clement Delafargue]

Je shoot un mail à la cantine.

Cordialement,
Clément Delafargue
cle...@delafargue.name
http://www.eklaweb.com

PGP Fingerprint : 5311 A6C4 8416 5378 3019 B977 FFB4 9299 EAE0 ED53

2013/1/24 Pierre-Alexandre Voye <ontol...@gmail.com>:

[Mogzor]

bon pour moi

2013/1/24 Clement Delafargue <cle...@delafargue.name>:

[Clement Delafargue]

J'ai eu la confirmation de la cantine. Je leur envoie la description
de la séance et je crée une page eventbrite demain dans la journée

Cordialement,
Clément Delafargue
cle...@delafargue.name
http://www.eklaweb.com

PGP Fingerprint : 5311 A6C4 8416 5378 3019 B977 FFB4 9299 EAE0 ED53

2013/1/25 Mogzor <mog...@gmail.com>:

[Clement Delafargue]

Complètement en retard, mais j'ai créé une page eventbrite :

http://www.eventbrite.com/event/5520164962

Si vous venez, pouvez-vous vous y inscrire svp ?
Merci d'avance et désolé pour le retard.

Cordialement,
Clément Delafargue
cle...@delafargue.name
http://www.eklaweb.com

PGP Fingerprint : 5311 A6C4 8416 5378 3019 B977 FFB4 9299 EAE0 ED53

2013/1/25 Clement Delafargue <cle...@delafargue.name>: