REasoning on CIrcular proofs for PROGramming


RECIPROG is an ANR collaborative project (aka. PRC) started in the fall 2021-2022 and running till the end of 2025. ReCiProg aims at extending the proofs-as-programs correspondence (also known as Curry-Howard correspondence) to recursive programs and circular proofs for logic and type systems using induction and coinduction. The project will contribute both to the necessary theoretical foundations of circular proofs and to the software development allowing to enhance the use of coinductive types and coinductive reasoning in the Coq proof assistant: such coinductive types present, in the current state of the art serious defects that the project will aim at solving.

The project is coordinated by Alexis Saurin and has four locations: IRIF in Paris, LIP in Lyon, LIS in Marseille and LS2N in Nantes.

Several positions will be available during the course of the project, funded by ANR or via other funding mechanisms. Look at the bottom of this page for specific announcements.


  • On the occasion of Abhishek De's defense, a mini-workshop will take place on december 1st and 2nd, 2022 in IRIF.
  • Abhishek De will defend his PhD entitled Linear Logic with least and greatest fixed points: Truth semantics, complexity and a parallel syntax on december 1st, 2022 in IRIF.
  • Emile Hazard defended his PhD entitled Non-determinism, explorable automata and cyclic proofs on september 30th, 2022 in LIP.
  • The project kick-off meeting took place in Lyon on may 6th, 2022!

Detailed presentation of the scientific program

A detailed description of RECIPROG scientific program can be found here.

Permanent researchers involved in RECIPROG

IRIF (Paris)
  • Thomas Ehrhrard (IRIF, CNRS)
  • Adrien Guatto (IRIF, Université de Paris)
  • Hugo Herbelin (IRIF, INRIA)
  • Pierre Hyvernat (LAMA, Université Savoie-Mont-Blanc)
  • Paul-André Melliès (IRIF, CNRS)
  • Daniel Petrişan (IRIF, Université de Paris)
  • Alexis Saurin (IRIF, CNRS – National coordinator & Paris local coordinator)
  • Benoît Valiron (LMF, Centrale Supélec)
LIP (Lyon)
  • Denis Kuperberg (LIP, CNRS – Lyon local coordinator)
  • Olivier Laurent (LIP, CNRS)
  • Matteo Mio (LIP, CNRS)
  • Damien Pous (LIP, CNRS)
  • Colin Riba (LIP, ENS Lyon)
  • Yannick Zakowski (LIP, INRIA)
LIS (Marseille)
  • Pierre CLairambault (LIS, CNRS)
  • Charles Grellois (LIS, Université d'Aix-Marseille)
  • Luigi Santocanale (LIS, Université d'Aix-Marseille – Marseille local coordinator)
  • Lionel Vaux (I2M, Université d'Aix-Marseille)
LS2N (Nantes)
  • Guilhem Jaber (LS2N, Université de Nantes – Nantes local coordinator)
  • Guillaume Munch-Maccagnoni (LS2N, INRIA)
  • Pierre-Marie Pédrot (L2SN, INRIA)
  • Matthieu Sozeau (LS2N, INRIA)

Job offers

  • The project is looking for post-docs: please contact Alexis Saurin, Guilhem Jaber and Denis Kuperberg for more informations.
  • The project will be hiring a PhD student in Marseille: please contact Luigi Santocanale and Pierre Hyvernat for more informations.