athena AT services.cnrs.fr
Objet : Histoire des techniques
Archives de la liste
[ATHENA] [Codes Sources] Anne-Gwen BOSSER et Pierre COURTIEU : Machines pour raconter, jeudi 1er juin 2023
Chronologique Discussions
- From: Baptiste Mélès <baptiste.meles AT gmail.com>
- Subject: [ATHENA] [Codes Sources] Anne-Gwen BOSSER et Pierre COURTIEU : Machines pour raconter, jeudi 1er juin 2023
- Date: Fri, 26 May 2023 09:03:04 +0200
Séminaire « Codes sources »
L'objectif du séminaire Codes sources est de présenter la pensée
informatique là où elle s'exprime le plus concrètement : dans les textes
que sont les codes sources.
Séance du jeudi 1er juin 2023 (IRILL, 14h-16h) :
Anne-Gwen BOSSER (ENIB, Lab-STICC CNRS UMR 6285, équipe COMMEDIA) et
Pierre COURTIEU (Cédric, Cnam) :
« Machines pour raconter »
Résumé :
Chez les humains, les histoires sont une forme de communication
utilisée pour faire sens du monde et de ce qui nous arrive, et les
tentatives de mécanisation de la production de récits pré-datent
largement les IA statistiques. La narration computationnelle a
d’ailleurs fourni la toile de fond pour plusieurs contributions à la
représentation des connaissances. Elle propose également un cadre
formel pour présenter des événements en suivant des objectifs
communicationnels précis.
Nous reviendrons sur nos travaux sur la formalisation et la
manipulation des structures narratives en logique linéaire, et en
particulier sur l’utilisation de l’assistant de preuve Coq pour
l’étude des propriétés formelles des récits interactifs. Plus
précisément, nous décrivons une méthode de modélisation des ressources
et des actions narratives, ainsi que des contraintes sur la fin de
l'histoire sous la forme d'un séquent ILL. Nous décrirons comment des
récits bien formés peuvent être interprétés à partir d'arbres de
preuve sans coupure du séquent obtenu à l'aide de Coq. Enfin, nous
décrivons comment raisonner sur les récits au niveau structurel à
l'aide de Coq : en permettant de prouver des propriétés du second
ordre sur l'ensemble de toutes les preuves générées par un séquent,
Coq facilite la vérification des propriétés structurelles des récits à
travers toutes ses variantes possibles.
Lieu :
en chair et en os à l'IRILL :
métro Jussieu (lignes 7 et 10), 4 place Jussieu, 75005 Paris
- rentrer dans le bâtiment Esclangon ;
- à gauche, emprunter l'escalier extérieur jusqu'au 1er étage ;
- sur le plateau SCAI, longer le tableau noir puis les baies vitrées ;
- la salle Séminaire se trouve au fond à gauche
ou par vidéoconférence :
https://galene.irill.org/group/irill/codessources/ (avec un
identifiant quelconque et un mot de passe vide)
------------------------------------------------------------------------
Prochaine séance du séminaire Codes sources :
- Jeudi 22 juin 2023 : Benoît VALIRON (CentraleSupélec, LMF) : calcul
quantique
------------------------------------------------------------------------
/* ***************************************
* À propos du séminaire Codes sources *
*************************************** */
À celui seul qui prend la peine de les lire effectivement, les codes
sources révèlent leur richesse. On y découvre que l'élégance d'un
algorithme réside parfois hors de sa complexité, dans l'usage virtuose
des idiomes du langage de programmation ou dans la connaissance fine de
la machine à laquelle il est destiné. Bien souvent des codes sources
comportent davantage de lignes de commentaires que de code. Tous ces
trésors de pensée informatique fondent à la compilation comme neige au
soleil — preuve qu'un programme n'est pas seulement écrit pour être
compilé.
Le but du séminaire est de décrire ces œuvres de l'esprit comme des
textes à part entière. Nous espérons ainsi contribuer à la constitution
d'une culture générale en programmation. En informatique comme en
littérature, cela suppose la familiarisation progressive avec un corpus
de grands textes.
À chaque séance, un intervenant — jeune chercheur ou chercheur confirmé
en informatique, en histoire ou en philosophie — présente, en moins
d'une heure, un code source de son choix : un fragment de système
d'exploitation, de pilote, de compilateur, de bibliothèque... Le code
peut avoir été écrit par l'orateur ou par quelqu'un d'autre, dans
quelque langage que ce soit. Le commentaire peut être algorithmique,
stylistique, historique ou philosophique, et porter sur tous les aspects
du code, commentaires compris. Le code est ensuite discuté avec
l'auditoire.
Organisateurs :
- Emmanuel Chailloux (LIP6, IRILL)
- Raphaël Fournier-S'niehotta (CNAM)
- Baptiste Mélès (CNRS, Archives Henri-Poincaré)
Site : http://codesource.hypotheses.org/
Contact : Baptiste Mélès (baptiste.meles AT univ-lorraine.fr)
Twitter : https://twitter.com/SemCodesSources
Liste de diffusion : https://groups.google.com/forum/#!forum/codes-sources
------------------------------------------------------------------------
--
Baptiste MÉLÈS
CNRS, Chargé de recherche / Researcher | http://baptiste.meles.free.fr/
Université de Lorraine, Université de Strasbourg, CNRS, AHP-PReST UMR 7117
91 avenue de la Libération, 54000 Nancy, France
Secrétaire des Amis de Jean Cavaillès | http://cavailles.hypotheses.org/
-
Pour une réponse rapide, n'hésitez pas à me téléphoner | Do not hesitate
to call me for a sooner response.
Attachment:
signature.asc
Description: PGP signature
- [ATHENA] [Codes Sources] Anne-Gwen BOSSER et Pierre COURTIEU : Machines pour raconter, jeudi 1er juin 2023, Baptiste Mélès, 26/05/2023
Archives gérées par MHonArc 2.6.19.