Archives de catégorie : Saison 2018-2019

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 » (13/06/2019)

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)

Gauthier van den Hove : « L’invention des liens statiques » (23/05/2019)

Gauthier van den Hove (Centrum Wiskunde & Informatica)

« L’invention des liens statiques »

Résumé

La plupart des langages de programmation utilisent une pile de blocs d’activation pendant leur exécution, dans laquelle les blocs d’activation sont liés entre eux par deux liens, communément appelés « dynamique » et « statique ». Notre exposé examinera l’invention de cette technique, et sa première mise en œuvre, en 1960, dans la première implémentation du langage ALGOL 60, qui est l’ancêtre de la plupart des langages de programmation dits « impératifs » utilisés aujourd’hui.

Informations

Jeudi 23 mai 2019

Salle 24-25/405 du LIP6 (rotonde 25, 4e étage)
4 place Jussieu, 75005 Paris
métro Jussieu (lignes 7 et 10)

Marie-José Durand-Richard : « Les diagrammes de fonctionnement de The Analytical Engine, de Charles Babbage 1791-1877) à Ada Lovelace (1815-1852) » (11/04/2019)

Marie-José Durand-Richard (Paris 8, SPHERE, CNRS)

« Les diagrammes de fonctionnement de The Analytical Engine, de Charles Babbage 1791-1877) à Ada Lovelace (1815-1852) »

Résumé

Charles Babbage (1791-1877) a élaboré les plans de The Analytical Engine afin de matérialiser la conception symbolique de l’algèbre élaborée au sein d’un réseau d’algébristes nommé The Analytics. Cette conception était fondée sur les propriétés strictement opératoires des développements en série. Suite à la présentation de ses plans en Italie en 1841, l’ingénieur militaire Luigi Menabrea (1809-1896) a publié en français quelques exemples de  diagrammes de fonctionnement de cette machine, diagrammes que je qualifie de statiques. Dans les précieuses notes qu’elle ajoute dans sa traduction de cet article en anglais, Ada Lovelace (1815-1852) les complète par de nouveaux diagrammes, que je qualifie de dynamiques. On étudiera ces diagrammes afin d’examiner quelles sont les caractéristiques qui peuvent permettre, ou non, de les qualifier de programmes.

Informations

Jeudi 11 avril 2019

Salle 24-25/405 du LIP6 (rotonde 25, 4e étage)
4 place Jussieu, 75005 Paris
métro Jussieu (lignes 7 et 10)

Bastien Guerry : « Code source et/ou documentation ? Réflexions autour de l’éditeur Emacs, du langage Emacs Lisp et du module Org-mode » (28/03/2019)

Orateur

Bastien Guerry

Titre

« Code source et/ou documentation ? Réflexions autour de l’éditeur Emacs, du langage Emacs Lisp et du module Org-mode »

Résumé

Cette présentation est un jalon le long d’une réflexion plus large sur la documentation logicielle. Une fois illustrés quelques problèmes généraux, nous explorerons la documentation de l’éditeur GNU Emacs et du langage Emacs Lisp d’un point de vue « utilisateur ». Puis nous aborderons cette question de la rédaction de la documentation du point de vue « développeur » à partir de notre expérience de la maintenance d’org-mode, un module d’Emacs. Un temps important sera consacré aux échanges pour que chacun puisse contraster ces expériences à l’aide d’autres expériences particulières.

Informations

Jeudi 28 mars 2019

Salle 25-26/105 du LIP6 (rotonde 25, 1er étage) (attention au changement de salle !)

4 place Jussieu, 75005 Paris
métro Jussieu (lignes 7 et 10)

Documents

  • Le site Write the Docs, mise en œuvre du projet décrit par Bastien Guerry dans cet exposé.

Assia Mahboubi, « Démonstrations assistées par ordinateur » (07/02/2019)

Assia MAHBOUBI (Inria, LS2N, Université de Nantes)

« Démonstrations assistées par ordinateur »

Informations pratiques

Jeudi 7 février 2019

Salle 24-25/405 du LIP6 (rotonde 25, 4e étage)

4 place Jussieu, 75005 Paris
métro Jussieu (lignes 7 et 10)

Affiche (PDF)

Résumé

Les ordinateurs ont profondément transformé la pratique des mathématiques contemporaines, mettant en particulier leur puissance de calcul au service de l’observation, de la conjecture et même de la validation “par calcul”. La généralisation rapide de l’accès à une puissance de calcul surhumaine a même suscité de nouvelles formes de mathématiques, à l’interface avec l’informatique, comme le calcul formel ou l’analyse numérique. Moins connus que certains systèmes de calcul symbolique, numérique ou statistique, les “assistants de preuve” font néanmoins partie des logiciels qui permettent de faire des mathématiques sur ordinateur. Ils sont conçus pour aider leurs utilisateurs à représenter définitions, énoncés et démonstrations dans un formalisme logique précis et non ambigu, sous la forme de bibliothèques digitales de mathématiques formalisées. Il existe plusieurs sous-familles d’assistants de preuves, qui diffèrent en particulier sur le choix de fondations logiques, qui détermine le langage formel utilisé. En particulier, une majorité d’entre eux sont basés sur une forme de théorie des types, une approche des fondations logiques qui donne une place privilégiée aux fonctions, et au concept de calcul. Mais dans tous les case, une telle (ré)écriture des théories mathématiques serait bien trop piétonne pour être envisageable, sinon intéressante, sans l’aide de la machine. Cette dernière permet en retour de réduire la vérification des preuves à une tâche routinière et mécanisée. Mais ce n’est pas le seul bénéfice d’une telle formalisation et nous discuterons dans cet exposé la pratique et les enjeux de cette forme de mathématiques assistées par ordinateur.

Cet exposé ne présuppose pas de connaissance particulière en logique ou en programmation.

Oriane Piquer-Louis : « Informatique et présentation de soi : la ligne de commande, une esthétique de l’efficacité ? Retour sur un mémoire de Master » (24/01/2019)

Oriane PIQUER-LOUIS (Université Lumière Lyon 2, ELICO)

« Informatique et présentation de soi : la ligne de commande, une esthétique de l’efficacité ? Retour sur un mémoire de Master »

Informations pratiques

Jeudi 24 janvier 2019, 14h-16h.

Salle 24-25/405 du LIP6 (rotonde 25, 4e étage)

4 place Jussieu, 75005 Paris

métro Jussieu (lignes 7 et 10)

Résumé

Comment une interface peut-elle influencer le rapport à soi, aux autres et à l’informatique ? Ce travail consiste à explorer les raisons qui poussent une certaine frange des utilisateurs d’ordinateurs à les configurer en ligne de commande, et à en étudier l’impact en termes de présentation de soi.

On remarque en effet que la ligne de commande génère autour d’elle une sociabilité assez particulière, nourrie par des imaginaires ambivalents et théâtralisés. C’est un objet sémiotique puissant, pris dans un réseau d’influences divers qui évoque à lui seul ce que nous avons appelé une esthétique de l’efficacité, ce rapport différent que l’on entretient avec l’informatique en adoptant cet outil. En effet, cette esthétique excède l’objet auquel elle est attachée-la ligne de commande-et vient couvrir des aspects de la vie quotidienne qui n’ont rien à voir avec l’informatique.

On reviendra sur les conclusions de ce travail, et sur les différentes pistes de recherche envisagées aujourd’hui.

Documents