Actes des Journées Francophones des Langages Applicatifs 2019
Notice bibliographique
Résumé
En 2019, les 30èmes journées francophones des langages applicatifs (JFLA) se déroulent aux Rousses dans le Jura.Après une édition méditerranéenne à Banyuls-sur-Mer, les JFLA retrouvent donc une nouvelle fois la montagne.Chaque année, les JFLA réunissent, dans un cadre convivial, des concepteurs, des développeurs et des utilisateurs des langages fonctionnels, des assistants de preuve et des outils de vérification de programmes en présentant des travaux variés, allant des aspects les plus théoriques aux applications industrielles.Cette année, nous avons sélectionné 11 articles de recherche et 4 articles courts.Les thématiques sont variées : preuve formelle, exécution symbolique, vérification de programmes, langages de programmation, mais aussi théorie des catégories et programmation synchrone.La sélection a été faite par les membres du comité de programme à partir des articles reçus après les 18 soumissions de résumés.Ceux-ci ont été aidés dans leur travail par des rapporteurs extérieurs que nous souhaitons remercier ici : Timothy Bourke, Adrien Guatto et Pascal Schreck.Cette année, le format des papiers courts permet de faire connaître à la communauté des JFLA des travaux en cours ou bien récemment publiés.Pour compléter le programme, nous bénéficions de deux cours, l'un par Guillaume Melquiond sur les liens entre l'arithmétique des ordinateurs et les preuves formelles; l'autre par Pierre-Marie Pédrot sur la prise en compte des effets dans la théorie des types.Nous assisterons également à deux exposés invités, le premier par Ilaria Castellani sur les types de session qui peuvent être vus comme une abstraction pour les protocoles de communication et le second par Pierre Courtieu sur l'étude formelle de protocoles de déplacement de robots.Enfin cette 30ème édition des JFLA est l'occasion de se retrouver et d'observer le chemin parcouru depuis quelques années.Nous avons sélectionné les 3 orateurs les plus prolifiques des 10 dernières éditions (2009 à 2018).Tous les 3 ont, chacun en ce qui les concerne, présenté au moins 7 contributions aux JFLA en 10 ans.Il s'agit de Jean-Christophe Filliâtre qui nous fera une synthèse de ses 25 années d'expérience(s) en programmation avec OCaml, de Louis Mandel qui fera un tour d'horizon de la programmation synchrone aux JFLA et d'Alan Schmitt qui nous parlera de sémantiques formelles certifiées.Nous remercions chaleureusement la cellule Congrès de l'Université de Strasbourg qui nous a accompagnée sur le chemin logistique et administratif des JFLA 2019: Christine Guibert, et surtout Marion Oswald, qui a été présente de bout en bout pour gérer tous les aléas administratifs rencontrés.Enfin, nos sincères remerciements à nos généreux sponsors.Cette année encore, les étudiants orateurs ne paient pas les frais d'hébergement et d'inscription.Merci au laboratoire ICube de l'Université de Strasbourg, au CEA LIST, au GDR GPL, à OcamlPro et à TrustInSoft.
Récupéré en direct depuis OpenAlex et désinversé. Les résumés ne sont pas conservés dans cette base de données : les index inversés représentent 8,6 Go des 9,3 Go de texte de la base, et le serveur dispose de 13 Go libres.
Comment cette classification a été obtenuedéplier
Prédiction machine sur la base complète
Imitation des enseignantsNi prévalence calibrée, ni vérité terrain. Validation humaine à venir. Le volet Gemma est une étiquette directe du modèle pour chaque travail de la base, lue sur la notice réduite au titre. Le volet Codex est un classifieur appris des 10 348 étiquettes directes de Codex et calibré sur les taux pondérés de l'échantillon; les champs sans appui suffisant ne portent aucun appel Codex. Le mode candidate est l'union des deux volets; le consensus est leur intersection. Ces sorties portent le statut machine_predicted_unvalidated et ne sont pas des étiquettes humaines.
Scores du classifieur distillé par catégorie (deux têtes)
| Catégorie | Codex | Gemma |
|---|---|---|
| Métarecherche | 0,007 | 0,027 |
| Méta-épidémiologie (sens strict) | 0,001 | 0,000 |
| Méta-épidémiologie (sens large) | 0,001 | 0,001 |
| Bibliométrie | 0,005 | 0,003 |
| Études des sciences et des technologies | 0,003 | 0,001 |
| Communication savante | 0,004 | 0,001 |
| Science ouverte | 0,001 | 0,002 |
| Intégrité de la recherche | 0,002 | 0,003 |
| Charge utile insuffisante (le modèle a refusé de juger) | 0,023 | 0,010 |
Scores machine (provisoires)
Les deux têtes enseignantes du modèle étudiant, lues sur ce travail. Un score ordonne la base pour la relecture; il n'affirme jamais une catégorie, et le statut de validation accompagne chaque rangée tel quel.
Scores de référence d'un modèle non mature (critères de maturité non atteints, 7 itérations). Un score ordonne; il n'affirme jamais une catégorie.
score_only:v0-immature-baseline · tel quel depuis la passe de notation : score_only signifie que le nombre peut ordonner les travaux, et qu'aucune étiquette de catégorie n'en découleClassification
machine, non validéePrédiction automatique; un appel candidat d’une seule source (Gemma direct ou Codex distillé), pas un consensus.
Le détail, modèle par modèle et score par score, se trouve en fin de page sous « Comment cette classification a été obtenue ».