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

Documents et médias

Télécharger le programme

pdf (366.45 Ko)

Programme

Cours

10:00 - 11:00

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

Xavier Leroy

05 déc 2018

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

05 déc 2018

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

12 déc 2018

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

12 déc 2018

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

19 déc 2018

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

19 déc 2018

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

09 jan 2019

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

09 jan 2019

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

16 jan 2019

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

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

Réalisabilité et forcing

Alexandre Miquel

16 jan 2019

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

23 jan 2019

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

23 jan 2019

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

30 jan 2019

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

30 jan 2019

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

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

30 jan 2019

11:30 - 12:30

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

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

Documents et médias

Programme

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

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

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

Les types dépendants : tout un programme !

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

Mathématiques assistées par ordinateur

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

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

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

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

Le forcing, une transformation de programme comme une autre ?

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

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

Réalisabilité et forcing

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

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

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

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

Voir aussi