{"word_count": 156, "character_count": 1173}
Guillaume Munch-Maccagnoni (Inria, Gallinette)« Curry-Howard et méthode en recherche en langages de programmation : l'exemple de l'objet comme valeur linéaire »RésuméLa logique linéaire est depuis longtemps annoncée comme porteuse d'une révolution pour le développement des langages de programmation. Où en est-on ? Le langage de programmation Rust est un récent langage industriel qui contient « de vrais morceaux » de logique linéaire assurant sa sûreté. Il est perçu comme une avancée majeure pour plusieurs champs d'application : programmation système, programmation concurrente. Mais on s'étonnera des canaux détournés empruntés par les idées de la logique linéaire avant de parvenir à leur application, à travers la programmation système et la programmation «&#160;objet&#160;».Je présenterai ces idées et proposerai de retracer une partie de leur évolution. Ce sera l'occasion de réfléchir au rôle de la correspondance de Curry-Howard dans la recherche sur le design des langages de&#160;programmation.InformationsJeudi 13 juin 2019Salle 24-25/405 du&#160;LIP6 (rotonde&#160;25, 4e&#160;étage)4&#160;place Jussieu, 75005 Parismétro Jussieu (lignes&#160;7 et&#160;10)