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 « objet ».
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 programmation.
Informations
Jeudi 13 juin 2019
Salle 24-25/405 du LIP6 (rotonde 25, 4e étage)
4 place Jussieu, 75005 Paris
métro Jussieu (lignes 7 et 10)