É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 @ 01 57 27 94 01 4026 Chargé.e de recherche - INRIA ISFP PPS preuves , picube , programmes 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 , programmes , preuves , picube Herbelin Hugo @ 01 57 27 90 87 3029 Directeur.rice de recherche - INRIA PPS algebre , picube , preuves , programmes Letouzey Pierre @ 01 57 27 93 37 3040 Maître.sse de conférences PPS picube , programmes , preuves Lévy Jean-Jacques @ 01 57 27 92 68 4032 Directeur.rice de recherche émérite - INRIA PPS preuves , picube , programmes 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 , programmes , preuves , picube Scherer Gabriel @ 01 57 27 92 68 4032 Chargé.e de recherche - INRIA PPS algebre , preuves , picube , programmes 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 Ait-Moussa Djamel @ 3035 Doctorant.e PPS algebre , picube Aristote Quentin @ 3010 Doctorant.e ASV , PPS automates , picube Baillon Martin @ 4029a Post-Doctorant.e PPS picube Behnia Sayna @ Doctorant.e PPS algebre , preuves , picube , programmes Bertrand Meven @ Post-Doctorant.e PPS picube Brede Nuria @ 4029a Post-Doctorant.e PPS picube Clemente Gabriella @ Post-Doctorant.e ASV , PPS automates , algebre , preuves , picube Gallego Emilio @ 01 57 27 92 68 4032 Starting research position - INRIA PPS algebre , preuves , picube , programmes Jubert Moana @ 3034 Doctorant.e PPS picube , algebre , preuves Kirst Dominik @ 4053 Post-Doctorant.e PPS preuves , picube , programmes Lahaye Sébastien @ 3035 Doctorant.e PPS picube 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 Reboullet Sarah @ 3044 Ingénieur.e de recherche PPS preuves , picube Suo Ariadne @ Doctorant.e PPS algebre , preuves , picube , programmes Viennot Jules @ 3044 Doctorant.e PPS picube Informations pratiques Partir en mission à l'INRIA Rapport d'activité 2020 de l'équipe Rapport d'activité 2020 de l'équipe (pdf)