Depuis l'an dernier, Xavier Leroy est le nouveau titulaire de la chaire « sciences du logiciel » auCollège de France. J'en avais fait unjournal pour présenter le thème de sa première année de cours où il abordait la correspondance entre programmes et démonstrations mathématiques, connue sous le nom decorrespondance de Curry-Howard.

Cette année, il a décidé d'aborder la formalisation de la sémantique des langages de programmation avec l'aide de la machine (en utilisant l'assistant de(…)

À partir de cette année l'informatique et les sciences du numériques se voient dotées d'une nouvelle chaire au Collège de France, intitulée « Sciences du logiciel », dont le titulaire estXavier Leroy. Xavier Leroy est connu pour être l'architecte et un des principaux développeurs du langage de programmation fonctionnelOCaml ainsi que du compilateur C formellement vérifiéCompCert.Il a reçu en 2016 le prix Milner pour récompenser ses travaux sur la fiabilité des systèmes informatiques.

La(…)

Au détour de mes pérégrinations sur la toile, je suis tombé sur un fil au contenu amusant et étonnant sur lestack exchange Unix. Mais que fait la commandeman après minuit ? Se transforme-t-elle en Gremlins si on lui donne à manger ? Non, elle se met à chanter ! mais à une heure bien précise. :-)

Ceteaster egg est resté confidentiel pendant 6 ans. Il fut introduit par cecommit et trouve son origine dansune blague faite sur(…)

Certains d’entre vous ont peut‐être vu passer l’information : les derniers processeurs Intel des familles Skylake et Kaby Lake sont victimes d’un bogue lorsque l’hyper‐threading est activé. On trouve par exempleun article surArs Technica, et Debianpropose des instructions détaillées pour corriger le problème en mettant à jour le microcode (firmware) du processeur.

Cette dépêche propose revenir sur les événements qui ont mené à la découverte du problème. Xavier Leroy le décrit en détail dans un article sur le blog de l’équipe Gallium, dont je proposerai un résumé pour les lecteurs francophones.

Certains d'entre vous ont peut-être vu passer l'information : les derniers processeurs Intel des familles Skylake et Kaby Lake sont victimes d'un bug lorsque l'hyperthreading est activé. On trouve par exempleun article sur Ars Technica, et Debianpropose des instructions détaillées pour corriger le problème en mettant à jour le firmware du CPU.

Néanmoins, dans ce journal, je vais revenir sur les événements qui ont mené à la découverte du problème. Xavier Leroy le décrit en détail(…)

La période électorale franco‐française arrive bientôt à son terme, ce qui nous a valu des journaux sur les systèmes de vote et d’autres, un peu plus gratinés, de colleurs d’affiches. Pendant ce temps, dans le monde du logiciel libre, une élection avait lieu de son côté : Debian élisait son nouveau responsable en la personne de Chris Lamb. Cette dépêche est l’occasion de revenir sur son déroulement et son résultat.

Le 17 avril, le projet Debian a apprisl'arrestation de Dmitry Bogatov (en) par les autorités russes.

Dmitry Bogatov est un enseignant en mathématiques, et un contributeur Debian actif. En tant que mainteneur Debian, par exemple, il travaillait dans le groupe Haskell et maintenait actuellement de nombreux paquets d'outils systèmes et en ligne de commande.

Pour le moment, les raisons de son arrestation et ce qui lui est reproché ne sont pas connues. Le projet a tout de même pris(…)

En cette période électoral, dans la lignée de certains journaux polémiques de ces derniers jours, je me devais de faire un journal pour relater le résultat d'une élection tombé hier. Non, il ne s'agit pas du résultat du référendum s'étant déroulé en Turquie ! On est sur LinuxFr.org, on y parle de logiciels libres et de ce qui gravite autour du libre en général. Je parlerais donc de l'élection du nouveauleader d'une des distributions majeures (et celle que j'utilise)(…)

Hier, jeudi 24 novembre 2016,Xavier Leroy a reçu leprix Milner à Londres à la Royal Society. Le prix Milner est le plus grand prix européen en informatique; il est décerné conjointement par la Royal Society, l'Académie des Sciences et l'académie allemande Leopoldina. Il est décerné en l'honneur de l'informaticien britanniqueRobin Milner qui fut lauréat du Prix Turing en 1992.

Le prix revient cette année à Xavier Leroy pour ses travaux tant théoriques que pratiques sur la fiabilité(…)

Dans la lignée du journalEDSL et F-algèbres, ce journal présente une méthode pour plonger un langage dans un autre (ici OCaml) qui généralise la précédente et centrée autour de la notion d'interprétation. Contrairement aux méthodes plus courantes pour résoudre cette question, la méthodetagless-final permet également de résoudre leproblème de l'extensibilité : étendre un type de donnés, ajouter des opérations dessus, sans avoir à réécrire du code déjà compilé et cela avec la sécurité du(…)

Pour la deuxième année consécutive, l'université Paris Diderot, en partenariat avec la Sorbonne, INRIA, IRILL et OCamlPro, organise un MOOC d'initiation à la programmation fonctionnelle avec le langage OCaml. Les leçons débuteront le 26 septembre 2016 et se termineront le 12 décembre. Les cours seront donnés en anglais mais des sous-titres sont disponibles aussi bien en anglais qu'en français. Il est toutefois possible de s'inscrire jusqu'au 25 novembre pour les retardataires.