→
Séminaire

Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

→
    du au
    Voir aussi :

    Documents et médias

    Programme

    Les chemins d'une découverte : la correspondance de Curry-Howard, 1930-1970
    Xavier Leroy

    -
    Cours
    Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui
    Amphithéâtre Guillaume-Budé, Site Marcelin-Berthelot
    -

    Polymorphisme à tous les étages ! Du système F au calcul des constructions
    Xavier Leroy

    -
    Cours
    Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui
    Amphithéâtre Guillaume-Budé, Site Marcelin-Berthelot
    -

    Des armes de construction massive : types inductifs et prédicats inductifs
    Xavier Leroy

    -
    Cours
    Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui
    Amphithéâtre Guillaume-Budé, Site Marcelin-Berthelot
    -

    Les types dépendants : tout un programme !
    Pierre-Évariste Dagand

    -
    Séminaire
    Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui
    Amphithéâtre Guillaume-Budé, Site Marcelin-Berthelot
    -

    Il faut qu'une porte soit ouverte ou fermée ! Logique classique, continuations, opérateurs de contrôle
    Xavier Leroy

    -
    Cours
    Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui
    Amphithéâtre Guillaume-Budé, Site Marcelin-Berthelot
    -

    Mathématiques assistées par ordinateur
    Assia Mahboubi

    -
    Séminaire
    Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui
    Amphithéâtre Guillaume-Budé, Site Marcelin-Berthelot
    -

    Peut-on changer le monde ? Programmation impérative, effets monadiques, effets algébriques
    Xavier Leroy

    -
    Cours
    Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui
    Amphithéâtre Guillaume-Budé, Site Marcelin-Berthelot
    -

    Programmer avec Coq : récursion et filtrage dépendant
    Matthieu Sozeau

    -
    Séminaire
    Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui
    Amphithéâtre Guillaume-Budé, Site Marcelin-Berthelot
    -

    Des théorèmes gratuits : la paramétricité
    Xavier Leroy

    -
    Cours
    Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui
    Amphithéâtre Guillaume-Budé, Site Marcelin-Berthelot
    -

    Peut-on dupliquer un objet ? Linéarité et contrôle des ressources
    Guillaume Munch-Maccagnoni

    -
    Séminaire
    Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui
    Amphithéâtre Guillaume-Budé, Site Marcelin-Berthelot
    -

    Le forcing, une transformation de programme comme une autre ?
    Xavier Leroy

    -
    Cours
    Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui
    Amphithéâtre Guillaume-Budé, Site Marcelin-Berthelot
    -

    À pas comptés : les techniques de step-indexing
    Xavier Leroy

    -
    Cours
    Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui
    Amphithéâtre Guillaume-Budé, Site Marcelin-Berthelot
    -

    Sisyphe heureux : types infinis, démonstrations par coinduction, et programmation réactive
    Xavier Leroy

    -
    Cours
    Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui
    Amphithéâtre Guillaume-Budé, Site Marcelin-Berthelot
    -

    Réalisabilité et forcing
    Alexandre Miquel

    -
    Séminaire
    Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui
    Amphithéâtre Guillaume-Budé, Site Marcelin-Berthelot
    -

    Qu'est-ce que l'égalité ? De Leibniz à la théorie homotopique des types
    Xavier Leroy

    -
    Cours
    Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui
    Amphithéâtre Guillaume-Budé, Site Marcelin-Berthelot
    -

    Sémantique des programmes fonctionnels probabilistes, à la lumière de la logique linéaire
    Christine Tasson

    -
    Séminaire
    Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui
    Amphithéâtre Guillaume-Budé, Site Marcelin-Berthelot
    -

    Du calcul des constructions à la théorie des types univalents
    Thierry Coquand

    -
    Séminaire
    Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui
    Amphithéâtre Guillaume-Budé, Site Marcelin-Berthelot
    -

    Conclusion, discussions et réponses aux questions de l'année
    Xavier Leroy

    -
    Cours
    Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui
    Amphithéâtre Guillaume-Budé, Site Marcelin-Berthelot
    -

    Voir aussi

    Cours en relation avec le séminaire : Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui
    Xavier Leroy, chaire Sciences du logiciel