É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 t probabilistes pour la programmaion, 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 les fondaments des mathématiques: théorie des types homotopiques, réalisabilité et forcing, logique linéaire différentielle, sémantique des langages de programmation: effects calculatoires, programmation différentielle et probabiliste, l'architecture et la conception des assistants de preuves: formalisation des mathematiques, unification et techniques symboliques d'élaboration de manière à réduire le fossée qui sépare actuellement le langage vernaculaire utlisé 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égrer de nouveaux ingrédients en direction des mathématiques certifiées, de la programmation différentielle et probabiliste et de l'apprentissage en vue de s'attaquer aux thématiques précédentes. Séminaire de l'équipe https://www.irif.fr/seminaires/picube/index Permanents en poste à l'IRIF Nom@TéléphoneBureauFonctionPôleÉquipe 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 picube , preuves , systemes Martinez Thierry @ 01 57 27 90 87 3029 Ingénieur de recherche - INRIA PPS 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 picube , algebre , systemes , preuves 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 Allioux Antoine @ 01 57 27 92 28 3034 Doctorant.e PPS picube , algebre , preuves Bauer Esaie @ 3033 Doctorant.e PPS preuves , picube Blazy Vincent @ 3044 Doctorant.e PPS picube , algebre , preuves Castro Felix @ 3026 Doctorant.e PPS picube , algebre , systemes , preuves Djuric Alen @ 3033 Post-Doctorant.e PPS algebre , 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 Moeneclaey Hugo @ 3034 Doctorant.e PPS picube , algebre , systemes , preuves Moreau Vincent @ 4033 Doctorant.e ASV , PPS automates , 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)