Équipe-projet Inria Pôle Preuves, programmes et systèmes Picube (Inria) Responsable Paul-André Melliès Thèmes de recherche L'équipe Picube est une équipe-projet commune à l'INRIA, à l'Université Paris-Cité et au CNRS, au sein du pôle Preuves, Programmes et Systèmes de l'IRIF. Elle couvre cinq thématiques principales de recherche : les structures fondamentales de la logique et du raisonnement mathématique ; les outils différentiels et probabilistes pour la programmation, le raisonnement et l'apprentissage ; l'architecture et la conception d'un assistant de preuves pour le mathématicien ; la formalisation et la linguistique des mathématiques ; L'algèbre de dimension supérieure et la théorie des types homotopiques. L'équipe Picube souhaite profiter des avancées récentes dans les domaines de: la théorie des types et des fondements des mathématiques: théorie des types homotopiques, réalisabilité et forcing, logique linéaire différentielle, la sémantique des langages de programmation: effets calculatoires, programmation différentielle et probabiliste, l'architecture et la conception des assistants de preuves: formalisation des mathématiques, unification et techniques symboliques d'élaboration de manière à réduire le fossé qui sépare actuellement le langage vernaculaire utilisé par les mathématiciens dans leur pratique quotidienne et le langage formel utilisé aujourd'hui dans les assistants de preuve comme Coq, Agda ou Lean. Le projet de recherche s'appuie sur les connaissances et l'expertise accumulée dans l'équipe Pi.R2 et y intégre de nouveaux ingrédients en direction des mathématiques certifiées, de la programmation différentielle et probabiliste et de l'apprentissage. Séminaire de l'équipe https://www.irif.fr/seminaires/picube/index Permanents en poste à l'IRIF Nom@TéléphoneBureauFonctionPôleÉquipe Baudart Guillaume @ 4026 Chargé.e de recherche - INRIA ISFP PPS systemes , preuves , picube Curien Pierre-Louis @ 01 57 27 92 23 3013 Directeur.rice de recherche émérite - CNRS PPS picube , algebre , preuves Ehrhard Thomas @ 01 57 27 92 17 4014a Directeur.rice de recherche - CNRS PPS algebre , systemes , preuves , picube Herbelin Hugo @ 01 57 27 90 87 3029 Directeur.rice de recherche - INRIA PPS algebre , picube , preuves , systemes Letouzey Pierre @ 01 57 27 93 37 3040 Maître.sse de conférences PPS picube , systemes , preuves Lévy Jean-Jacques @ 01 57 27 92 68 3009 Directeur.rice de recherche émérite - INRIA PPS systemes , preuves , picube Melliès Paul-André @ 01 57 27 92 48 3023 Directeur.rice de recherche - CNRS ASV , PPS automates , algebre , preuves , picube Petrisan Daniela @ 01 57 27 94 00 4016 Maître.sse de conférences ASV , PPS automates , algebre , picube Saurin Alexis @ 01 57 27 93 37 3040 Chargé.e de recherche - CNRS PPS algebre , systemes , preuves , picube Scherer Gabriel @ 4032 Chargé.e de recherche - INRIA PPS algebre , systemes , preuves , picube Permanents en poste hors de l'IRIF Nom@TéléphoneBureauFonctionSiteÉquipe Marino Diana @ 01 80 49 40 39 A218 Assistante de l'Équipe CRI Paris picube Mathurin Anne @ 01 80 49 40 37 A118 Assistante de l'Équipe CRI Paris picube Non-permanents Nom@TéléphoneBureauFonctionPôleÉquipe Aristote Quentin @ 3010 Doctorant.e ASV , PPS automates , picube Bauer Esaie @ 3033 Doctorant.e PPS preuves , picube Belloundja Abdelkader @ Stagiaire PPS preuves , systemes , algebre , picube Blanchi Victor @ Stagiaire PPS picube Blazy Vincent @ 3044 Doctorant.e PPS picube , algebre , preuves Brasseur Leopold @ Stagiaire PPS algebre , systemes , preuves , picube Castro Felix @ 3026 Doctorant.e PPS picube , algebre , systemes , preuves Danilkin Anton @ Stagiaire PPS systemes , picube , preuves Djuric Alen @ 3033 Post-Doctorant.e PPS algebre , picube Fiorillo Guido @ Stagiaire PPS algebre , systemes , preuves , picube Gallego Emilio @ 01 57 27 92 24 4030 Starting research position - INRIA PPS picube , algebre , systemes , preuves Jafar-Rhamani Farzad @ 01 57 27 92 92 3026 Post-Doctorant.e PPS algebre , systemes , preuves , picube Jubert Moana @ 3034 Doctorant.e PPS picube , algebre , preuves Martinez Thierry @ 01 57 27 90 87 3029 Ingénieur.e de recherche - INRIA PPS preuves , picube Moreau Vincent @ 4033 Doctorant.e ASV , PPS automates , picube , algebre Osorio Daniel @ Stagiaire PPS systemes , preuves , picube , algebre Reboullet Sarah @ 3034 Doctorant.e PPS preuves , picube Informations pratiques Partir en mission à l'INRIA Rapport d'activité 2020 de l'équipe Rapport d'activité 2020 de l'équipe (pdf)