Équipe-projet Inria


Responsable


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

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


Informations pratiques