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 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 picube , preuves , systemes Martinez Thierry @ 01 57 27 90 87 3029 Research ingenior - INRIA PPS 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 picube , algebre , systemes , preuves Non-permanent members Name@PhoneOfficePositionPoleTeam Allioux Antoine @ 01 57 27 92 28 3034 PhD Student PPS picube , algebre , preuves Bauer Esaie @ 3033 PhD Student PPS preuves , picube Blazy Vincent @ 3044 PhD Student PPS picube , algebre , preuves Castro Felix @ 3026 PhD Student PPS picube , algebre , systemes , preuves Djuric Alen @ 3033 Post-Doc 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-Doc PPS algebre , systemes , preuves , picube Jubert Moana @ 3034 PhD Student PPS picube , algebre , preuves Moeneclaey Hugo @ 3034 PhD Student PPS picube , algebre , systemes , preuves Moreau Vincent @ 4033 PhD Student ASV , PPS automates , picube , algebre Reboullet Sarah @ 3034 PhD Student PPS preuves , picube