Partager Facebook X (ex-Twitter) Linkedin Copier le lien Agenda 87 événements Filtres Dates Close Dates Dates Du Au 7 prochains jours 30 prochains jours Professeur, chaire, laboratoire Close Professeur, chaire, laboratoire Professeur, chaire, laboratoire Rechercher un professeur, une chaire ou un laboratoire Xavier Leroy (2018 - aujourd'hui) Domaines Close Domaines Domaines (-) Mathématiques et sciences informatiques (87) Type d'enseignement Close Type d'enseignement Type d'enseignement Cours (48) Séminaire (37) Leçon inaugurale (1) Conférencier invité (1) Filtres actifs Xavier Leroy (2018 - aujourd'hui) Mathématiques et sciences informatiques 15 nov 2018 Leçon inaugurale 18:00 - 19:00 Le logiciel, entre l'esprit et la matière Xavier Leroy 15 nov 2018 Amphithéâtre Marguerite de Navarre, Site Marcelin Berthelot 15 nov 2018 18:00 - 19:00 21 nov 2018 Cours 10:00 - 11:00 Les chemins d'une découverte : la correspondance de Curry-Howard, 1930-1970 Xavier Leroy 21 nov 2018 Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 21 nov 2018 10:00 - 11:00 Cours 11:30 - 12:30 Polymorphisme à tous les étages ! Du système F au calcul des constructions Xavier Leroy 21 nov 2018 Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 21 nov 2018 11:30 - 12:30 28 nov 2018 Cours 10:00 - 11:00 Des armes de construction massive : types inductifs et prédicats inductifs Xavier Leroy 28 nov 2018 Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 28 nov 2018 10:00 - 11:00 Séminaire 11:30 - 12:30 Les types dépendants : tout un programme ! Pierre-Évariste Dagand 28 nov 2018 Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 28 nov 2018 11:30 - 12:30 05 déc 2018 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 05 déc 2018 10:00 - 11:00 Séminaire 11:30 - 12:30 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 05 déc 2018 11:30 - 12:30 12 déc 2018 Cours 10:00 - 11:00 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 12 déc 2018 10:00 - 11:00 Séminaire 11:30 - 12:30 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 12 déc 2018 11:30 - 12:30 19 déc 2018 Cours 10:00 - 11:00 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 19 déc 2018 10:00 - 11:00 Séminaire 11:30 - 12:30 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 19 déc 2018 11:30 - 12:30 09 jan 2019 Cours 10:00 - 11:00 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 09 jan 2019 10:00 - 11:00 Cours 11:30 - 12:30 À 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 09 jan 2019 11:30 - 12:30 16 jan 2019 Cours 10:00 - 11:00 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 16 jan 2019 10:00 - 11:00 Séminaire 11:30 - 12:30 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 16 jan 2019 11:30 - 12:30 23 jan 2019 Cours 10:00 - 11:00 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 23 jan 2019 10:00 - 11:00 Séminaire 11:30 - 12:30 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 23 jan 2019 11:30 - 12:30 30 jan 2019 Séminaire 10:00 - 11:00 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 30 jan 2019 10:00 - 11:00 Cours 11:30 - 12:30 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 18 Mar 2019 Conférencier invité 17:00 - 18:00 Concurrent Connected Components Robert E. Tarjan 18 Mar 2019 Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 18 Mar 2019 17:00 - 18:00 28 nov 2019 Cours 09:30 - 11:00 Des expressions et des commandes : la sémantique d'un langage impératif Xavier Leroy 28 nov 2019 Sémantiques mécanisées : quand la machine raisonne sur ses langages Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 28 nov 2019 09:30 - 11:00 12 déc 2019 Cours 09:30 - 11:00 Traduttore, traditore : vérification formelle d'un compilateur Xavier Leroy 12 déc 2019 Sémantiques mécanisées : quand la machine raisonne sur ses langages Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 12 déc 2019 09:30 - 11:00 Séminaire 11:15 - 12:15 Lambda, the Ultimate Teaching Assistant (Agda Version) Philip Wadler 12 déc 2019 Sémantiques mécanisées : quand la machine raisonne sur ses langages Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 12 déc 2019 11:15 - 12:15 19 déc 2019 Cours 09:30 - 11:00 Compiler mieux : optimisations, analyses statiques, et leur vérification Xavier Leroy 19 déc 2019 Sémantiques mécanisées : quand la machine raisonne sur ses langages Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 19 déc 2019 09:30 - 11:00 Séminaire 11:15 - 12:15 L'arithmétique des ordinateurs et sa formalisation Sylvie Boldo 19 déc 2019 Sémantiques mécanisées : quand la machine raisonne sur ses langages Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 19 déc 2019 11:15 - 12:15 09 jan 2020 Cours 09:30 - 11:00 Des logiques pour raisonner sur les programmes Xavier Leroy 09 jan 2020 Sémantiques mécanisées : quand la machine raisonne sur ses langages Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 09 jan 2020 09:30 - 11:00 Séminaire 11:15 - 12:15 Sémantique formelle de JavaScript : les enjeux du passage à l'échelle Alan Schmitt 09 jan 2020 Sémantiques mécanisées : quand la machine raisonne sur ses langages Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 09 jan 2020 11:15 - 12:15 16 jan 2020 Cours 09:30 - 11:00 Un art abstrait : l'analyse statique par interprétation abstraite Xavier Leroy 16 jan 2020 Sémantiques mécanisées : quand la machine raisonne sur ses langages Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 16 jan 2020 09:30 - 11:00 Séminaire 11:15 - 12:15 Logique de séparation en Coq : théorie et pratique Arthur Charguéraud 16 jan 2020 Sémantiques mécanisées : quand la machine raisonne sur ses langages Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 16 jan 2020 11:15 - 12:15 30 jan 2020 Cours 09:30 - 11:00 L'éternité, c'est long : divergence, théorie des domaines, approches coinductives Xavier Leroy 30 jan 2020 Sémantiques mécanisées : quand la machine raisonne sur ses langages Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 30 jan 2020 09:30 - 11:00 Pagination Page courante 1 Page 2 Page 3 Page suivante Dernière page
Leçon inaugurale 18:00 - 19:00 Le logiciel, entre l'esprit et la matière Xavier Leroy 15 nov 2018 Amphithéâtre Marguerite de Navarre, Site Marcelin Berthelot 15 nov 2018 18:00 - 19:00
Cours 10:00 - 11:00 Les chemins d'une découverte : la correspondance de Curry-Howard, 1930-1970 Xavier Leroy 21 nov 2018 Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 21 nov 2018 10:00 - 11:00
Cours 11:30 - 12:30 Polymorphisme à tous les étages ! Du système F au calcul des constructions Xavier Leroy 21 nov 2018 Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 21 nov 2018 11:30 - 12:30
Cours 10:00 - 11:00 Des armes de construction massive : types inductifs et prédicats inductifs Xavier Leroy 28 nov 2018 Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 28 nov 2018 10:00 - 11:00
Séminaire 11:30 - 12:30 Les types dépendants : tout un programme ! Pierre-Évariste Dagand 28 nov 2018 Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 28 nov 2018 11:30 - 12:30
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 05 déc 2018 10:00 - 11:00
Séminaire 11:30 - 12:30 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 05 déc 2018 11:30 - 12:30
Cours 10:00 - 11:00 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 12 déc 2018 10:00 - 11:00
Séminaire 11:30 - 12:30 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 12 déc 2018 11:30 - 12:30
Cours 10:00 - 11:00 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 19 déc 2018 10:00 - 11:00
Séminaire 11:30 - 12:30 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 19 déc 2018 11:30 - 12:30
Cours 10:00 - 11:00 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 09 jan 2019 10:00 - 11:00
Cours 11:30 - 12:30 À 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 09 jan 2019 11:30 - 12:30
Cours 10:00 - 11:00 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 16 jan 2019 10:00 - 11:00
Séminaire 11:30 - 12:30 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 16 jan 2019 11:30 - 12:30
Cours 10:00 - 11:00 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 23 jan 2019 10:00 - 11:00
Séminaire 11:30 - 12:30 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 23 jan 2019 11:30 - 12:30
Séminaire 10:00 - 11:00 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 30 jan 2019 10:00 - 11:00
Cours 11:30 - 12:30 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
Conférencier invité 17:00 - 18:00 Concurrent Connected Components Robert E. Tarjan 18 Mar 2019 Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 18 Mar 2019 17:00 - 18:00
Cours 09:30 - 11:00 Des expressions et des commandes : la sémantique d'un langage impératif Xavier Leroy 28 nov 2019 Sémantiques mécanisées : quand la machine raisonne sur ses langages Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 28 nov 2019 09:30 - 11:00
Cours 09:30 - 11:00 Traduttore, traditore : vérification formelle d'un compilateur Xavier Leroy 12 déc 2019 Sémantiques mécanisées : quand la machine raisonne sur ses langages Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 12 déc 2019 09:30 - 11:00
Séminaire 11:15 - 12:15 Lambda, the Ultimate Teaching Assistant (Agda Version) Philip Wadler 12 déc 2019 Sémantiques mécanisées : quand la machine raisonne sur ses langages Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 12 déc 2019 11:15 - 12:15
Cours 09:30 - 11:00 Compiler mieux : optimisations, analyses statiques, et leur vérification Xavier Leroy 19 déc 2019 Sémantiques mécanisées : quand la machine raisonne sur ses langages Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 19 déc 2019 09:30 - 11:00
Séminaire 11:15 - 12:15 L'arithmétique des ordinateurs et sa formalisation Sylvie Boldo 19 déc 2019 Sémantiques mécanisées : quand la machine raisonne sur ses langages Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 19 déc 2019 11:15 - 12:15
Cours 09:30 - 11:00 Des logiques pour raisonner sur les programmes Xavier Leroy 09 jan 2020 Sémantiques mécanisées : quand la machine raisonne sur ses langages Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 09 jan 2020 09:30 - 11:00
Séminaire 11:15 - 12:15 Sémantique formelle de JavaScript : les enjeux du passage à l'échelle Alan Schmitt 09 jan 2020 Sémantiques mécanisées : quand la machine raisonne sur ses langages Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 09 jan 2020 11:15 - 12:15
Cours 09:30 - 11:00 Un art abstrait : l'analyse statique par interprétation abstraite Xavier Leroy 16 jan 2020 Sémantiques mécanisées : quand la machine raisonne sur ses langages Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 16 jan 2020 09:30 - 11:00
Séminaire 11:15 - 12:15 Logique de séparation en Coq : théorie et pratique Arthur Charguéraud 16 jan 2020 Sémantiques mécanisées : quand la machine raisonne sur ses langages Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 16 jan 2020 11:15 - 12:15
Cours 09:30 - 11:00 L'éternité, c'est long : divergence, théorie des domaines, approches coinductives Xavier Leroy 30 jan 2020 Sémantiques mécanisées : quand la machine raisonne sur ses langages Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 30 jan 2020 09:30 - 11:00