Structures de contrôle : de « goto » aux effets algébriques (3) - Xavier Leroy (2023-2024)

Enseignement 2023-2024 : Structures de contrôle : de « goto » aux effets algébriques Cours du 8 février 2024 : Chassez le contrôle... : la programmation déclarative La programmation déclarative s'attache à décrire les résultats attendus du programme sans pour autant expliciter l'enchaînement des étapes de calcul élémentaires qui produisent ces résultats, au contraire de la programmation impérative classique. Avons-nous encore besoin de structures de contrôle dans les programmes déclaratifs ? Le troisième cours a tenté de répondre à cette question en prenant l'exemple de trois paradigmes de programmation déclarative : la programmation réactive synchrone (Lustre), la programmation purement fonctionnelle (Haskell, Scheme pur), et la programmation logique (Prolog). Les sémantiques des programmes écrits dans ces langages reposent sur des principes élégants mais qui ne suffisent pas pour garantir la terminaison et le coût (en temps, en espace) des exécutions d'un programme ; d'où l'importance, même dans un langage déclaratif, de donner aux programmeurs les moyens de contrôler la manière dont leurs programmes sont évalués. Nous avons mentionné trois de ces moyens : ajouter des opérations ad hoc comme la coupure en Prolog, spécifier les stratégies d'évaluation utilisées (comme l'appel par valeur en Scheme et l'appel par nécessité en Haskell), ou encoder la stratégie désirée dans le programme lui-même (par exemple en ajoutant des suspensions dans un programme Scheme). Professeur : Xavier Leroy Chaire Sciences du logiciel 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

11 Feb 2024

Collège de France - Sciences du logiciel

View Video
Structures de contrôle : de « goto » aux effets algébriques (3) - Xavier Leroy (2023-2024)

Enseignement 2023-2024 : Structures de contrôle : de « goto » aux effets algébriques Cours du 8 février 2024 : Chassez le contrôle... : la programmation déclarative La programmation déclarative s'attache à décrire les résultats attendus du programme sans pour autant expliciter l'enchaînement des étapes de calcul élémentaires qui produisent ces résultats, au contraire de la programmation impérative classique. Avons-nous encore besoin de structures de contrôle dans les programmes déclaratifs ? Le troisième cours a tenté de répondre à cette question en prenant l'exemple de trois paradigmes de programmation déclarative : la programmation réactive synchrone (Lustre), la programmation purement fonctionnelle (Haskell, Scheme pur), et la programmation logique (Prolog). Les sémantiques des programmes écrits dans ces langages reposent sur des principes élégants mais qui ne suffisent pas pour garantir la terminaison et le coût (en temps, en espace) des exécutions d'un programme ; d'où l'importance, même dans un langage déclaratif, de donner aux programmeurs les moyens de contrôler la manière dont leurs programmes sont évalués. Nous avons mentionné trois de ces moyens : ajouter des opérations ad hoc comme la coupure en Prolog, spécifier les stratégies d'évaluation utilisées (comme l'appel par valeur en Scheme et l'appel par nécessité en Haskell), ou encoder la stratégie désirée dans le programme lui-même (par exemple en ajoutant des suspensions dans un programme Scheme). Professeur : Xavier Leroy Chaire Sciences du logiciel 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

11 Feb 2024

Collège de France - Sciences du logiciel

View Video
Cooperation and Lwt.pause

11 Feb 2024

Romain Calascibetta

Read Article
Inferring Locality in OCaml | OCaml Unboxed

This is the fourth video in a series about OCaml’s locals. It covers how the compiler infers what variables can be marked as local_ and it gives a glimpse into some compiler output that you can use to see the inferred modes on variables. I also explain how the compiler infers conversions between locals and globals and introduce *mode-crossing*, showing how ints can be both local and global. View instructions to get the compiler I use in this video: https://github.com/janestreet/opam-repository/tree/with-extensions

07 Feb 2024

Jane Street - OCaml Unboxed

View Video
Inferring Locality in OCaml | OCaml Unboxed

This is the fourth video in a series about OCaml’s locals. It covers how the compiler infers what variables can be marked as local_ and it gives a glimpse into some compiler output that you can use to see the inferred modes on variables. I also explain how the compiler infers conversions between locals and globals and introduce *mode-crossing*, showing how ints can be both local and global. View instructions to get the compiler I use in this video: https://github.com/janestreet/opam-repository/tree/with-extensions

07 Feb 2024

Jane Street - OCaml Unboxed

View Video
Improving OCaml.org to Provide an Engaging UX and Trusted User Resources

The OCaml.org team, which includes members from Tarides, have been working hard to improve OCaml.org. In the first half of 2023, our primary…

07 Feb 2024

Tarides

Read Article
Profiling Dune Builds

Co-authored with Louis Roché.

05 Feb 2024

Ahrefs

Read Article