This is an announcement for several one-year postdoctoral positions funded by the ANR ReCiProg - Reasoning on Circular proofs for Programming.

• Proof theory
• Curry-Howard correspondence
• Logics with fixed points
• Coinductive reasoning
• Proof assistants (formalization skills or development experience)
• Type theory
• Category theory
• Categorical logic
• Automated deduction
• Automata theory

In relation with the above topics, an experience in one or several of the following topics will be particularly appreciated: fixed-points and circular proofs, the Coq proof assistant, inductive and coinductive types, guarded recursion, coalgebras, inductive and coinductive theorem proving.

• LIP (Plume Team), Lyon (local coordinator: Denis Kuperberg)
• LS2N (Gallinette Team), Nantes (local coordinator: Guilhem Jaber)
• IRIF (PPS & Picube Team), Paris (local coordinator: Alexis Saurin)

Scientific projects involving two or more sites of the project are welcome.

• Please contact as soon as possible the project coordinator and the local coordinators of interest to discuss adequacy of your profil and express your intent to submit an application.
• Deadline for applications is on April 30th 2024, for a starting date between september 1st 2024 and december 31st 2024, to be negotiated.
• Candidates can send their application to Alexis Saurin (alexis dot saurin at irif dot fr) with a subject containing “[RECIPROG post-doc application]“.
• The application should contain a CV, a brief research statement (1-2 pages) & at least two contacts of reference persons (or reference letters if available).
• The salary will depend on the successful candidate's prior research experience with a guaranteed minimum of 2300 EUR/month before taxes.
• Each position is for a one-year post-doc.

RECIPROG is an ANR collaborative project (aka. PRC) starting in the fall 2021-2022 and running till the end of 2025. ReCiProg aims at extending the proofs-as-programs correspondence (aka Curry-Howard correspondence) to recursive programs and circular proofs for logics 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.

• More informations can be found on the project webpage: https://www.irif.fr/reciprog/index
• Interested candidates may contact the project coordinator (Alexis Saurin) as well as the local coordinators (Guilhem Jaber, Denis Kuperberg, Luigi Santocanale & Alexis Saurin).