RECIPROG REasoning on CIrcular proofs for PROGramming Overview 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. News Workshop on Coq guard condition, 3rd of june 2024 in Nantes. Three post-doc positions are open this spring for a start between september 1st and december 31st 2024. We will organize EPIT 2025! FICS 2024 took place in february in Naples After FICS 2023 organized by Denis Kuperberg, Alexis Saurin will organize FICS 2024 in Naples: consider submitting! Grégory Chichéry started his ANR-dunded PhD at LIS under the joint supervision of Pierre Hyvernat and Luigi Santocanale. Farzad Jafarrhamani defended his PhD entitled Fixpoints of types in linear logic from a Curry-Howard-Lambek perspective on january 25th, 2023 in IRIF. Kostia Chardonnet defended his PhD entitled Towards a Curry-Howard correspondence for quantum computation on january 9th, 2023 in Saclay. On the occasion of Abhishek De's defense, a mini-workshop took place on december 1st and 2nd, 2022 in IRIF. Abhishek De defended 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 Ehrhard (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 December 2021 post-doc offer 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.