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.

https://www.irif.fr/seminaires/picube/index