Inria project-team Pole Proofs, programs and systems Picube (Inria) Head Paul-André Melliès Research themes The Picube team is a joint project-team of INRIA, Université Paris-Cité and CNRS, within the IRIF's Proofs, Programs and Systems pole. It covers five main research themes: the fundamental structures of logic and mathematical reasoning ; differential and probabilistic tools for programming, reasoning and learning; architecture and design of a proof assistant for mathematicians; formalization and linguistics of mathematics; higher-dimensional algebra and homotopic type theory. The Picube team wishes to take advantage of recent advances in the fields of: type theory and the foundations of mathematics: homotopic type theory, realizability and forcing, differential linear logic, semantics of programming languages: computational effects, differential and probabilistic programming, architecture and design of proof assistants: mathematical formalization, unification and symbolic elaboration techniques. in order to reduce the gap between the vernacular language currently used by mathematicians in their daily practice and the formal language used today in proof assistants such as Coq, Agda or Lean. The research project builds on the knowledge and expertise accumulated in the Pi.R2 team and integrates new ingredients in the direction of certified mathematics, differential and probabilistic programming and learning, with a view to tackling the above themes. Team seminar https://www.irif.fr/seminaires/picube/index Permanent members Members outside of IRIF Name@PhoneOfficePositionLocationTeam Marino Diana @ 01 80 49 40 39 A218 Team assistant CRI Paris picube Mathurin Anne @ 01 80 49 40 37 A118 Team assistant CRI Paris picube Non-permanent members Permanent members Name@PhoneOfficePositionPoleTeam Baudart Guillaume @ 4026 Research Scientist - INRIA ISFP PPS systemes , preuves , picube Curien Pierre-Louis @ 01 57 27 92 23 3013 Senior Research Scientist Emeritus - CNRS PPS picube , algebre , preuves Ehrhard Thomas @ 01 57 27 92 17 4014a Senior Research Scientist - CNRS PPS algebre , systemes , preuves , picube Herbelin Hugo @ 01 57 27 90 87 3029 Senior Research Scientist - INRIA PPS algebre , picube , preuves , systemes Letouzey Pierre @ 01 57 27 93 37 3040 Associate Professor PPS picube , systemes , preuves Lévy Jean-Jacques @ 01 57 27 92 68 3009 Senior Research Scientist Emeritus - INRIA PPS systemes , preuves , picube Melliès Paul-André @ 01 57 27 92 48 3023 Senior Research Scientist - CNRS ASV , PPS automates , algebre , preuves , picube Petrisan Daniela @ 01 57 27 94 00 4016 Associate Professor ASV , PPS automates , algebre , picube Saurin Alexis @ 01 57 27 93 37 3040 Research Scientist - CNRS PPS algebre , systemes , preuves , picube Scherer Gabriel @ 4032 Research Scientist - INRIA PPS algebre , systemes , preuves , picube Non-permanent members Name@PhoneOfficePositionPoleTeam Aristote Quentin @ 3010 PhD Student ASV , PPS automates , picube Bauer Esaie @ 3033 PhD Student PPS preuves , picube Belloundja Abdelkader @ Intern PPS preuves , systemes , algebre , picube Blanchi Victor @ Intern PPS picube Blazy Vincent @ 3044 PhD Student PPS picube , algebre , preuves Brasseur Leopold @ Intern PPS algebre , systemes , preuves , picube Castro Felix @ 3026 PhD Student PPS picube , algebre , systemes , preuves Danilkin Anton @ Intern PPS systemes , picube , preuves Djuric Alen @ 3033 Post-Doc PPS algebre , picube Fiorillo Guido @ Intern 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-Doc PPS algebre , systemes , preuves , picube Jubert Moana @ 3034 PhD Student PPS picube , algebre , preuves Martinez Thierry @ 01 57 27 90 87 3029 Research ingenior - INRIA PPS preuves , picube Moreau Vincent @ 4033 PhD Student ASV , PPS automates , picube , algebre Osorio Daniel @ Intern PPS algebre , systemes , preuves , picube Reboullet Sarah @ 3034 PhD Student PPS preuves , picube