#### 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

#### Permanent members

#### Members outside of IRIF

#### Non-permanent members

#### Permanent members

Name | @ | Phone | Office | Position | Pole | Team |
---|---|---|---|---|---|---|

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 | @ | Phone | Office | Position | Pole | Team |
---|---|---|---|---|---|---|

Aristote Quentin | @ | 3010 | PhD Student | ASV , PPS | automates , picube | |

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 | |

Martinez Thierry | @ | 01 57 27 90 87 | 3029 | Research ingenior - INRIA | PPS | preuves , picube |

Moreau Vincent | @ | 4033 | PhD Student | ASV , PPS | automates , picube , algebre | |

Reboullet Sarah | @ | 3034 | PhD Student | PPS | preuves , picube |