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 @ 01 57 27 94 01 4026 Research Scientist - INRIA ISFP PPS preuves , picube , programmes 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 , programmes , preuves , picube Herbelin Hugo @ 01 57 27 90 87 3029 Senior Research Scientist - INRIA PPS algebre , picube , preuves , programmes Letouzey Pierre @ 01 57 27 93 37 3040 Associate Professor PPS picube , programmes , preuves Lévy Jean-Jacques @ 01 57 27 92 68 4032 Senior Research Scientist Emeritus - INRIA PPS preuves , picube , programmes 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 , programmes , preuves , picube Scherer Gabriel @ 4032 Research Scientist - INRIA PPS algebre , programmes , preuves , picube Non-permanent members Name@PhoneOfficePositionPoleTeam Aristote Quentin @ 3010 PhD Student ASV , PPS automates , picube Gallego Emilio @ 01 57 27 92 68 4032 Starting research position - INRIA PPS algebre , preuves , picube , programmes Jubert Moana @ 3034 PhD Student PPS picube , algebre , preuves Kirst Dominik @ 4053 Post-Doc PPS preuves , picube , programmes Martinez Thierry @ 01 57 27 90 87 3029 Research ingenior - INRIA PPS preuves , picube Mathieu Adrien @ Intern PPS preuves , picube , programmes Moreau Vincent @ 4033 PhD Student ASV , PPS automates , picube , algebre Reboullet Sarah @ 3034 PhD Student PPS preuves , picube Viennot Jules @ 3044 PhD Student PPS picube