Welcome, dear reader, to a new opam blog post! Today we take an additional step down the metaphorical rabbit hole with opam pin, the easiest way to catch a ride on the development version of a package in opam. We are aware that our readers are eager to see these blog posts venture on the developer s...
The OCaml 5 update brought much-anticipated support for programming on multiple cores. It also introduced support for concurrency via effect…
In this first post of the Flambda2 Snippets, we dive into the powerful CPS-based internal representation used within the Flambda2 optimizer, which was one of the main motivation to move on from the former Flambda optimizer. Credit goes to Andrew Kennedy's paper Compiling with Continuations, Continue...
Welcome to The Flambda2 Snippets! In this first post of The Flambda2 Snippets, we dive into the powerful CPS-based internal representation used within the Flambda2 optimizer, which was one of the main motivation to move on from the former Flambda optimizer. Credit goes to Andrew Kennedy's paper Comp...
Enseignement 2023-2024 : Structures de contrôle : de « goto » aux effets algébriques Séminaire du 14 mars 2024 : Design and Compilation of Efficient Effect Handlers in the Koka Language Intervenant : Daan Leijen, Microsoft Research Retrouvez les enregistrements audios et vidéos du cycle et son texte de présentation : https://www.college-de-france.fr/fr/agenda/seminaire/structures-de-controle-de-goto-aux-effets-algebriques Chaire Sciences du logiciel Professeur : Xavier Leroy Retrouvez tous les enseignements du Pr Xavier Leroy : https://www.college-de-france.fr/chaire/xavier-leroy-sciences-du-logiciel-chaire-statutaire https://www.youtube.com/playlist?list=PLtimy8tnozICbD45yhB7Ha_zIBJTIK3im Le Collège de France est une institution de recherche fondamentale dans tous les domaines de la connaissance et un lieu de diffusion du « savoir en train de se faire » ouvert à tous. Les cours, séminaires, colloques sont enregistrés puis mis à disposition du public sur le site internet du Collège de France. Découvrez toutes les ressources du Collège de France : https://www.college-de-france.fr Suivez-nous sur : Facebook : https://www.facebook.com/College.de.France Instagram : https://www.instagram.com/collegedefrance X (ex-Twitter) : https://twitter.com/cdf1530 LinkedIn : https://fr.linkedin.com/company/collègedefrance
Enseignement 2023-2024 : Structures de contrôle : de « goto » aux effets algébriques Séminaire du 14 mars 2024 : Design and Compilation of Efficient Effect Handlers in the Koka Language Intervenant : Daan Leijen, Microsoft Research Retrouvez les enregistrements audios et vidéos du cycle et son texte de présentation : https://www.college-de-france.fr/fr/agenda/seminaire/structures-de-controle-de-goto-aux-effets-algebriques Chaire Sciences du logiciel Professeur : Xavier Leroy Retrouvez tous les enseignements du Pr Xavier Leroy : https://www.college-de-france.fr/chaire/xavier-leroy-sciences-du-logiciel-chaire-statutaire https://www.youtube.com/playlist?list=PLtimy8tnozICbD45yhB7Ha_zIBJTIK3im Le Collège de France est une institution de recherche fondamentale dans tous les domaines de la connaissance et un lieu de diffusion du « savoir en train de se faire » ouvert à tous. Les cours, séminaires, colloques sont enregistrés puis mis à disposition du public sur le site internet du Collège de France. Découvrez toutes les ressources du Collège de France : https://www.college-de-france.fr Suivez-nous sur : Facebook : https://www.facebook.com/College.de.France Instagram : https://www.instagram.com/collegedefrance X (ex-Twitter) : https://twitter.com/cdf1530 LinkedIn : https://fr.linkedin.com/company/collègedefrance
Enseignement 2023-2024 : Structures de contrôle : de « goto » aux effets algébriques Cours du 14 mars 2024 : Logiques de programmes pour le contrôle et les effets Professeur : Xavier Leroy Chaire Sciences du logiciel Tout comme la logique mathématique donne des lois pour raisonner sur les définitions et les énoncés mathématiques, une logique de programmes pour un langage de programmation donne des lois pour établir des propriétés vraies de toutes les exécutions possibles d'un programme écrit dans ce langage. Après des rappels sur cette approche déductive de la vérification de programmes et sur la plus ancienne de ces logiques, celle publiée par C.A.R. Hoare en 1969, ce cours a montré comment cette logique de Hoare s'applique à de nombreuses structures de contrôle, dont plusieurs formes de boucles, avec sortie prématurée mono-niveau ou multi-niveaux, mais aussi à des constructions non-déterministes comme les commandes gardées de Dijkstra, et jusqu'aux coroutines asymétriques et aux threads coopératifs vus au deuxième cours. Même le branchement « goto » peut être spécifié en logique de Hoare, en prenant quelques précautions. Lire la suite : https://www.college-de-france.fr/fr/agenda/cours/structures-de-controle-de-goto-aux-effets-algebriques/logiques-de-programmes-pour-le-controle-et-les-effets Retrouvez les enregistrements audios et vidéos du cycle et son texte de présentation : https://www.college-de-france.fr/fr/agenda/cours/structures-de-controle-de-goto-aux-effets-algebriques Retrouvez tous les enseignements du Pr Xavier Leroy : https://www.college-de-france.fr/chaire/xavier-leroy-sciences-du-logiciel-chaire-statutaire https://www.youtube.com/playlist?list=PLtimy8tnozICbD45yhB7Ha_zIBJTIK3im Le Collège de France est une institution de recherche fondamentale dans tous les domaines de la connaissance et un lieu de diffusion du « savoir en train de se faire » ouvert à tous. Les cours, séminaires, colloques sont enregistrés puis mis à disposition du public sur le site internet du Collège de France. Découvrez toutes les ressources du Collège de France : https://www.college-de-france.fr Suivez-nous sur : Facebook : https://www.facebook.com/College.de.France Instagram : https://www.instagram.com/collegedefrance X (ex-Twitter) : https://twitter.com/cdf1530 LinkedIn : https://fr.linkedin.com/company/collègedefrance
