The OCaml Planet

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

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

At OCamlPro, the main ongoing task on the OCaml Compiler is to improve the high-level optimisation. This is something that we have been doing for quite some time now. Indeed, we are the authors behind the Flambda optimisation pass and today we would like to introduce the series of blog snippets show...

Introducing our Flambda2 snippets At OCamlPro, the main ongoing task on the OCaml Compiler is to improve the high-level optimisation. This is something that we have been doing for quite some time now. Indeed, we are the authors behind the Flambda optimisation pass and today we would like to introduc...

This video introduces the OCaml Unboxed series, which will dive into topics like local mode, unboxed types, and many more fun detours along the way. Join me, Richard Eisenberg, as we explore the frontiers of functional programming language design in OCaml! Oxidizing OCaml blog posts: - Locality: https://blog.janestreet.com/oxidizing-ocaml-locality - Ownership: https://blog.janestreet.com/oxidizing-ocaml-ownership - Data-race Freedom: https://blog.janestreet.com/oxidizing-ocaml-parallelism

This video introduces the OCaml Unboxed series, which will dive into topics like local mode, unboxed types, and many more fun detours along the way. Join me, Richard Eisenberg, as we explore the frontiers of functional programming language design in OCaml! Oxidizing OCaml blog posts: - Locality: https://blog.janestreet.com/oxidizing-ocaml-locality - Ownership: https://blog.janestreet.com/oxidizing-ocaml-ownership - Data-race Freedom: https://blog.janestreet.com/oxidizing-ocaml-parallelism

There are plenty of exciting computer programming events happening in India, including the 5 day OCaml retreat that Tarides is hosting in…

Enseignement 2023-2024 : Structures de contrôle : de « goto » aux effets algébriques Séminaire du 07 mars 2024 : Effect Handlers and Mathematically Inspired Language Constructs Intervenant : Matija Pretnar, Université de Ljubljana 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 07 mars 2024 : Effect Handlers and Mathematically Inspired Language Constructs Intervenant : Matija Pretnar, Université de Ljubljana 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