Tout d'abord merci à tous et toutes pour vos participations actives et constructives durant l'évènement de fin d'année de l'IRIF. Merci à la commission égalité d'avoir porté ce projet. Merci à vous tous et toutes de porter ces valeurs d'inclusion à l'IRIF et au delà.

La semaine prochaine nous aurons le dernier conseil de laboratoire de l'année, qui sera assez symbolique lui aussi. En effet, il s'agira d'un conseil de laboratoire extraordinaire avec les responsables d'équipe, mais aussi ouvert à tous et toutes, dont un des points à l'ordre du jour et l'avis du conseil de laboratoire sur la prochaine direction de l'IRIF.

Ne manquez pas non plus les demandes de bourses doctorales de l'Université qui doivent être déposées au plus tard le 15 juin. Pour la mise en place des recrutements sur projets de doctorant·e·s et postdoctorant·e·s, pensez aussi à démarrer la procédure au plus tôt.

Si vous êtes doctorant·e·s, ou si vous encadrez une thèse, n'oubliez pas la compagne d'inscription à une mission d'enseignement durant la thèse. Cette démarche est essentielle pour la carrière des doctorant·e·s et pour le bon fonctionnement de l'UFR Informatique (le département d'enseignement associé à l'IRIF).

Nous annonçons aussi une mise à jour dans la réservation et l'utilisation des salles, et rappelons les délais pour préparer vos voyages professionnels.

Côté actualités scientifiques, toujours plusieurs évènements en juin, ainsi que 4 nouveaux papiers IRIF acceptés cette fois-ci à TYPES22.

Enfin, durant les prochaines semaines, des extraits d'articles sélectionnés du magazine Quanta Magazine vont seront proposés dans nos focus. Nous commençons par un interview de Leslie Lamport du mois dernier.

Bonne lecture !

• Conseil de laboratoire extraordinaire avec responsables d'équipe : Mardi 14 juin 13h - Salle 3052 - Ouvert à tous et toutes
  • Nomination de 2 nouveaux responsables d’équipe thématique de l’IRIF
  • Point budget : état et analyse des dépenses sur la subvention annuelle de l’IRIF, ajustement des prévisions
  • Point sur les profils MCF/PR 2023 demandés par l'UFR
  • Examen de la proposition de nouvelle direction de l’IRIF : Profession de foi de Giuseppe Castagna et Thomas Colcombet

• Campagne Candidatures Contrats Doctoraux ED386
  • La date limite d’envoi des dossiers est fixée au mercredi 15 juin 2022. Toutes les informations relatives à la composition du dossier sont disponibles sur le site http://www.math.univ-paris-diderot.fr/formations/doctorats/index première rubrique « CD ED386 2022/2023 »
  • Data Intelligence Institute of Paris / Demi-bourse ED 386 : Le Diip financera cette année une demie-bourse de thèse pour l'ED 386 UPC. Pour le financement DiiP, constituer le même dossier juste en précisant que c'est pour cette bourse spécifique, et préciser la nature du co-financement.

• Mission d'enseignement pour doctorants
  • Cette mission n'est pas obligatoire mais très fortement recommandée et demandée par l'IRIF. La mission d’enseignement fait partie de notre profession. Les doctorants et doctorantes doivent y être associés au plus tôt, à la fois pour leur carrière, mais aussi pour assurer un bon fonctionnement de département d'enseignement.
  • L'IRIF demande donc à tous les doctorantes et doctorants d'assurer durant les 3 années de leur thèse :
    • Pour un·e doctorant·e francophone : au moins 2 et si possible 3 années de mission d’enseignement
    • Pour un·e doctorant·e non-francophone : au moins 1 et si possible 2 années de mission d’enseignement (après apprentissage du français)
  • Pour candidater pour la première fois à une mission d'enseignement en informatique avec les enseignants-chercheurs de l'IRIF, les candidatures doivent être déposées avant le 24 juin 2022. Toutes les informations à ce propos sont disponibles sur la page web suivante : http://www.informatique.univ-paris-diderot.fr/ufr/doctorants/accueil

• Recrutements sur projets (ANR/ERC/FSMP/…) : Merci de contacter dès maintenant secretariat@irif.fr pour les recrutements de septembre et octobre. Il convient de respecter 3 mois de délais. Plus d'informations : ressources_humaines. Avec les congés au milieu ces délais sont donc très stricts.

• Conflits dans les réservations de salle - Usages adaptés
  • En raison de plusieurs conflits de réservation de la salle 3058 de conseil de l'UFR dûs à une double gestion informatique de cette salle (système de réservation IRIF, système de réservation Université) qui ne résiste pas au pic de réservation en cette période de jurys, cette salle est de nouveau réservable uniquement par email au secrétariat et destinée en priorité aux activités liées à l'enseignement.
  • En retour, merci de réserver la salle 3052 que pour des activités liées à la recherche. Plus d'information Salles et espaces de travail.
  • Une recherche de nouveaux espaces devra être menée à la rentrée pour gérer la pénurie de place de l'IRIF.

• Missions and invitations
  • Please prepare your request at least two weeks before; one month in the case of a mission to or an invitation from an at-risk country .
  • Housing in France must be done within University and CNRS platforms by law. Exceptions are only negotiable for long visits (starting from 3 weeks) and for travelers with their family.

• Four papers coauthored by IRIF members will be presented at the conference TYPES'22, the main conference on types for proofs and programs, this summer.

• Workshops in June related to IRIF activities
  • Workshop Labyrinth of Combinatorics in memory of Pierre Rosenstiehl, June 15-17, Université Paris Cité
  • Workshop on Differentiable Programming, June 29-30, Université Paris Cité
  • Colloque Probabilistic Programming, June 29-30, Collège de France

Leslie Lamport revolutionized how computers talk to each other. Now he’s working on how engineers talk to their machines.

Leslie Lamport may not be a household name, but he’s behind a few of them for computer scientists: the typesetting program LaTeX and the work that made cloud infrastructure at Google and Amazon possible. He’s also brought more attention to a handful of problems, giving them distinctive names like the bakery algorithm and the Byzantine Generals Problem. This is no accident. The 81-year-old computer scientist is unusually thoughtful about how people use and think about software.

In 2013, he won the A.M. Turing Award, considered the Nobel Prize of computing, for his work on distributed systems, where multiple components on different networks coordinate to achieve a common objective. Internet searches, cloud computing and artificial intelligence all involve orchestrating legions of powerful computing machines to work together. Of course, this kind of coordination opens you up to more problems.

“A distributed system is one in which the failure of a computer you didn’t even know existed can render your own computer unusable,” Lamport once said.

Among the biggest sources of problems are “concurrent systems,” where multiple computing operations happen during overlapping slices of time, leading to ambiguity: Which computer’s clock is the right one? In a seminal 1978 paper, Lamport introduced the notion of “causality” to solve this issue, using an insight from special relativity. Two observers may disagree on the order of events, but if one event causes another, that eliminates the ambiguity. And sending or receiving a message can establish causality among multiple processes. Logical clocks — now also called Lamport clocks — provided a standard way to reason about concurrent systems.

With this tool in hand, computer scientists next wondered how they could systematically make these connected computers even bigger, without adding bugs. Lamport came up with an elegant solution: Paxos, a “consensus algorithm” that allows multiple computers to execute complex tasks. Without Paxos and its family of algorithms, modern computing could not exist.

In the early 1980s, as he developed the field, Lamport also created LaTeX, a document preparation system that provides sophisticated ways to typeset complex formulas and format scientific documents. LaTeX has become the standard for formatting papers not only in math and computer science but also in most scientific domains.

Lamport’s work since the 1990s has focused on “formal verification,” the use of mathematical proofs to verify the correctness of software and hardware systems. Notably, he created a “specification language” called TLA+ (for Temporal Logic of Actions). A software specification is like a blueprint or a recipe for a program; it describes how software should behave on a high level. It’s not always necessary, since coding a simple program is akin to just boiling an egg. But a more complicated task with higher stakes — the coding equivalent of a nine-course banquet — requires more precision. You need to prepare each component of each dish, combine them in a precise way, then serve them to every guest in the correct order. This requires exact recipes and instructions, written in unambiguous and succinct language, but descriptions written in English prose could leave room for misinterpretation. TLA+ employs the precise language of mathematics to prevent bugs and avoid design flaws.

Read his interview for Quantamagazine entitled How to Write Software With Mathematical Perfection.

Newsletter des partenaires : Les lettres arrivent sporadiquement aux membres de l'IRIF. Elles sont donc listées ci-dessous.

• CNRS Hebdo du 10/06/2022
• L'actualité de la Faculté des Sciences du 10/06/2022