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.
A detailed description of RECIPROG scientific program can be found here.