641 épisodes

Podcast du Collège de France

Collège de France (Sciences et technologies‪)‬ Collège de France

    • Cours
    • 3.8 • 45 notes

Podcast du Collège de France

    • video
    01 - Algorithmes quantiques

    01 - Algorithmes quantiques

    Frédéric Magniez
    Collège de France
    Informatique et sciences numériques (chaire annuelle)
    Algorithmes quantiques

    • 1h 30 min
    01 - Algorithmes quantiques

    01 - Algorithmes quantiques

    Frédéric Magniez
    Collège de France
    Informatique et sciences numériques (chaire annuelle)
    Algorithmes quantiques

    • 1h 30 min
    • video
    Leçon inaugurale - Frédéric Magniez - Informatique et sciences numériques (chaire annuelle) - VIDEO

    Leçon inaugurale - Frédéric Magniez - Informatique et sciences numériques (chaire annuelle) - VIDEO

    Frédéric Magniez
    Collège de France
    Informatique et sciences numériques (chaire annuelle)
    Leçon inaugurale : Algorithmes quantiques : quand la physique quantique défie la thèse de Church-Turing
    Tous les calculs informatiques sont actuellement exécutés sur des ordinateurs contraints par les lois de la physique newtonienne, dite encore physique classique. Cependant, comme l'a suggéré Richard Feynman dans les années 80, un ordinateur quantique pourrait tirer profit des phénomènes de superposition et d'intrication de la physique quantique afin d'accélérer ses calculs. Alors que des prototypes d'ordinateur quantique encore très limités voient progressivement le jour, start-up, grandes entreprises du numérique et aussi gouvernements orientent peu à peu leur recherche, stratégie et financement afin d’être prêts à exploiter le potentiel de ce futur ordinateur.

    En partant des premiers paradoxes quantiques, la leçon inaugurale et le cours prononcé dans le cadre de cette chaire présenteront les fondements de la cryptographie et de la communication quantiques. Ensuite, nous introduirons les concepts du calcul quantique par le biais des circuits, qui nous permettront de présenter les principales méthodes algorithmiques quantiques : mise en évidence de propriétés algébriques permettant de déchiffrer les messages secrets, et optimisation ouvrant la voie à un vaste champ d'applications algorithmiques. Puis nous aborderons les limites du calcul quantique, qu'elles soient théoriques ou liées aux technologies actuelles. Enfin, nous terminerons en décrivant une partie de la recherche actuelle motivée par l'utilisation à court terme de prototypes d'ordinateurs quantiques limités, mais pouvant potentiellement trouver des applications concrètes, comme notamment en intelligence artificielle ou encore en usage décentralisé de type Internet.

    • 51 min
    Leçon inaugurale - Frédéric Magniez - Informatique et sciences numériques (chaire annuelle)

    Leçon inaugurale - Frédéric Magniez - Informatique et sciences numériques (chaire annuelle)

    Frédéric Magniez
    Collège de France
    Informatique et sciences numériques (chaire annuelle)
    Leçon inaugurale : Algorithmes quantiques : quand la physique quantique défie la thèse de Church-Turing
    Tous les calculs informatiques sont actuellement exécutés sur des ordinateurs contraints par les lois de la physique newtonienne, dite encore physique classique. Cependant, comme l'a suggéré Richard Feynman dans les années 80, un ordinateur quantique pourrait tirer profit des phénomènes de superposition et d'intrication de la physique quantique afin d'accélérer ses calculs. Alors que des prototypes d'ordinateur quantique encore très limités voient progressivement le jour, start-up, grandes entreprises du numérique et aussi gouvernements orientent peu à peu leur recherche, stratégie et financement afin d’être prêts à exploiter le potentiel de ce futur ordinateur.

    En partant des premiers paradoxes quantiques, la leçon inaugurale et le cours prononcé dans le cadre de cette chaire présenteront les fondements de la cryptographie et de la communication quantiques. Ensuite, nous introduirons les concepts du calcul quantique par le biais des circuits, qui nous permettront de présenter les principales méthodes algorithmiques quantiques : mise en évidence de propriétés algébriques permettant de déchiffrer les messages secrets, et optimisation ouvrant la voie à un vaste champ d'applications algorithmiques. Puis nous aborderons les limites du calcul quantique, qu'elles soient théoriques ou liées aux technologies actuelles. Enfin, nous terminerons en décrivant une partie de la recherche actuelle motivée par l'utilisation à court terme de prototypes d'ordinateurs quantiques limités, mais pouvant potentiellement trouver des applications concrètes, comme notamment en intelligence artificielle ou encore en usage décentralisé de type Internet.

    • 51 min
    • video
    05 - Logiques de programmes : quand la machine raisonne sur ses logiciels - VIDEO

    05 - Logiques de programmes : quand la machine raisonne sur ses logiciels - VIDEO

    Xavier Leroy
    Collège de France
    Science du logiciel
    Année 2020-2021
    Logiques de programmes : quand la machine raisonne sur ses logiciels

    Dans le cinquième cours, nous avons étudié quatre extensions des logiques de séparation des précédents cours qui permettent ou facilitent la spécification et la vérification d'une plus large classe de programmes.

    La première extension est l'opérateur d'implication séparante, familièrement appelé « baguette magique » en raison de sa forme, qui est l'adjoint de la conjonction séparante, au même titre que l'implication usuelle est l'adjoint de la conjonction usuelle. Cette « baguette magique » facilite le raisonnement en logique de séparation, notamment via la règle de conséquence ramifiée ou via un calcul de plus faibles préconditions.

    La deuxième extension permet de vérifier des processus qui partagent des données mais y accèdent en lecture seule, sans modifications. Il s'agit d'associer des permissions aux cellules de la mémoire, ces permissions pouvant être partielles (permettant uniquement la lecture) ou complètes (permettant aussi l'écriture et la libération). Deux modèles bien connus de permissions partielles sont les permissions fractionnaires et les permissions comptées. Nous avons illustré l'utilisation de ces dernières pour vérifier un verrou à lecteurs multiples implémenté par deux sémaphores.

    Le « code fantôme » est la troisième technique étudiée dans cette séance. Il s'agit de commandes qui ne sont pas exécutées dans le programme final, mais contribuent à définir des « variables fantômes » qui simplifient la vérification. Dans le cadre du calcul parallèle, code et variables fantômes permettent de garder trace des calculs faits par chacun des processus et comment ces calculs individuels contribuent à l'exécution globale du programme.

    La dernière extension que nous avons décrite permet de stocker en mémoire des verrous et leur invariant de ressources, tout comme les données protégées par ces verrous. Cela permet de spécifier et de vérifier des algorithmes parallèles à grain fin, comme nous l'avons illustré avec une structure de liste simplement chaînée avec verrouillage couplé.

    Aussi disparates qu'elles peuvent sembler, ces extensions et bien d'autres sont des cas particuliers d'un petit nombre de notions plus générales, comme le montre l'infrastructure logique Iris.

    • 1h 22 min
    05 - Logiques de programmes : quand la machine raisonne sur ses logiciels

    05 - Logiques de programmes : quand la machine raisonne sur ses logiciels

    Xavier Leroy
    Collège de France
    Science du logiciel
    Année 2020-2021
    Logiques de programmes : quand la machine raisonne sur ses logiciels

    Dans le cinquième cours, nous avons étudié quatre extensions des logiques de séparation des précédents cours qui permettent ou facilitent la spécification et la vérification d'une plus large classe de programmes.

    La première extension est l'opérateur d'implication séparante, familièrement appelé « baguette magique » en raison de sa forme, qui est l'adjoint de la conjonction séparante, au même titre que l'implication usuelle est l'adjoint de la conjonction usuelle. Cette « baguette magique » facilite le raisonnement en logique de séparation, notamment via la règle de conséquence ramifiée ou via un calcul de plus faibles préconditions.

    La deuxième extension permet de vérifier des processus qui partagent des données mais y accèdent en lecture seule, sans modifications. Il s'agit d'associer des permissions aux cellules de la mémoire, ces permissions pouvant être partielles (permettant uniquement la lecture) ou complètes (permettant aussi l'écriture et la libération). Deux modèles bien connus de permissions partielles sont les permissions fractionnaires et les permissions comptées. Nous avons illustré l'utilisation de ces dernières pour vérifier un verrou à lecteurs multiples implémenté par deux sémaphores.

    Le « code fantôme » est la troisième technique étudiée dans cette séance. Il s'agit de commandes qui ne sont pas exécutées dans le programme final, mais contribuent à définir des « variables fantômes » qui simplifient la vérification. Dans le cadre du calcul parallèle, code et variables fantômes permettent de garder trace des calculs faits par chacun des processus et comment ces calculs individuels contribuent à l'exécution globale du programme.

    La dernière extension que nous avons décrite permet de stocker en mémoire des verrous et leur invariant de ressources, tout comme les données protégées par ces verrous. Cela permet de spécifier et de vérifier des algorithmes parallèles à grain fin, comme nous l'avons illustré avec une structure de liste simplement chaînée avec verrouillage couplé.

    Aussi disparates qu'elles peuvent sembler, ces extensions et bien d'autres sont des cas particuliers d'un petit nombre de notions plus générales, comme le montre l'infrastructure logique Iris.

    • 1h 22 min

Avis d’utilisateurs

3.8 sur 5
45 notes

45 notes

Classement des podcasts dans Cours

D’autres se sont aussi abonnés à

Plus par Collège de France