envoi du 4 octobre

bertot_bio.tex

+\subsection*{CV. de l'auteur}
+Yves Bertot est chercheur à l'Inria depuis 1992.  Il s'est spécialisé
+dans les preuves en theorie des types, étudiant successivement les
+propriétés des langages de programmation, la géométrie algorithmique,
+les flux infinis coinductifs, les
+calculs mathématiques et les interaction entre preuve formelle et
+calcul formel algébrique.  Il a co-écrit avec Pierre
+Castéran le premier livre sur le système Coq qui a été publié en 2004.  Yves
+Bertot a participé à certains des résultats les plus remarquables
+obtenus avec le système Coq, comme le compilateur Compcert et la
+preuve vérifiée sur ordinateur du théorème de l'ordre impair.
+
+Lien vers une photo: \url{https://www-sop.inria.fr/members/Yves.Bertot/Yves.Bertot-2021.jpg}.

intro_prog_fun.tex

@@ -58,7 +58,21 @@ coût est en moyenne logarithmique vis-à-vis de la taille du tableau.
 Pour cette raison, la programmation fonctionnelle pure est parfois
 évitée dans le développement de programmes efficaces.
 
-Toutefois, lorsque l'on s'intéresse à la correction des programmes, la
+Les cas d'usage de la programmation fonctionnelle sont très variés et
+touchent souvent des domaines où le coût des erreurs serait
+catastrophique: applications bancaires, blockchains, trading à haute
+fréquence.  Dans ces domaines, un avantage souvent cité est la
+grande lisibilité par des experts du domaine d'application
+(financiers, traders) tout en permettant une programmation très sûre.
+D'autres exemples d'application concernent
+des outils de programmation comme des compilateurs ou des analyseurs
+pour d'autres langages de programmation, comme le langage C
+(compilateur CompCert) ou des outils de preuve et de vérification de
+programmes, comme le langage Coq ou FramaC.  Pour ces applications,
+c'est la facilité à programmer sans erreur avec de nouveaux types de
+données qui est souvent appréciée.
+
+Lorsque l'on s'intéresse à la correction des programmes, la
 programmation fonctionnelle pure est un outil puissant.  D'une part,
 il existe des programmes pour lesquels l'efficacité des programmes
 fonctionnels pur suffit.  Mais même lorsque
@@ -74,7 +88,7 @@ Cette approche permet de vérifier par exemple qu'une relation est bien
 satisfaite entre l'état initial et l'état final du programme étudié,
 ou bien qu'une certaine propriété est satisfaite dans l'état final.
 
-Ici, nous ne montrerons pas comment établir une correspondance entre
-programmes à effets de bords et programmes en programmation
-fonctionnelle pure.  Nous nous concentrons sur la preuve de propriétés
-pour ces derniers.
+Dans cette première partie, nous ne montrerons pas comment établir une
+correspondance entre programmes à effets de bords et programmes en
+programmation fonctionnelle pure.  Nous nous concentrons sur la
+preuve de propriétés pour ces derniers.

short_article.tex

@@ -2,11 +2,13 @@
 \usepackage[utf8]{inputenc}
 \usepackage[french]{babel}
 \usepackage{hyperref}
-\title{Prouvez que vos programmes fonctionnels n'ont pas de bugs avec Coq}
+\title{Prouvez que vos programmes fonctionnels n'ont pas de bugs avec Coq\\
+Première partie}
 
 \author{Yves Bertot}
 \begin{document}
 \maketitle
+\input bertot_bio.tex
 \input intro_prog_fun.tex
 \input abstract_transfer.tex
 \subsection*{Conclusion}