Post-doc position in RECIPROG project (located in Lyon, Nantes or Paris)

[Alexis Saurin IRIF <alexis.saurin@irif.fr>]

This is an announcement for a postdoctoral position funded by the ANR
ReCiProg - Reasoning on Circular proofs for Programming.

*We seek candidates holding a PhD in Computer Science or Mathematics, and
with expertise in one or several of the following areas:*
- Proof theory
- Curry-Howard correspondence
- Logics with fixed points
- Coinductive reasoning
- Proof assistants
- Type theory
- Category theory
- Automated deduction

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.


*The successful candidate will be employed in one of the following French
research lab, depending on her/his specific profile:*- 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)

*Application process:*
- Deadline for applications is on January 5th 2022, for a starting date in
the first trimester of 2022, 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.

*Project summary*
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*
- More informations can be found on the project webpage:
https://www.irif.fr/reciprog/index and
https://www.irif.fr/reciprog/post-doc-offer-dec2021
- RECIPROG ANR project will open further positions in the coming two years,
including two more postdoctoral positions in the above teams, and a PhD
position in LIRICA Team, LIS, Marseille.
- Interested candidates may contact the project coordinator (Alexis Saurin)
as well as the local coordinators (Guilhem Jaber, Denis Kuperberg, Luigi
Santocanale & Alexis Saurin).


--
Alexis Saurin
IRIF - CNRS, Université de Paris & INRIA


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]