[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
This is an announcement for three one-year postdoctoral positions funded
by the ANR ReCiProg - Reasoning on Circular proofs for Programming, to
be hosted in Lyon (LIP), Nantes (LS2N, Gallinette) and Paris (IRIF,
PPS).
We seek strong 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 (formalization skills or development experience)
*
Type theory
*
Category theory
*
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, categorical logic, infinitary term rewriting and infinitary
lambda-calculi.
The successful candidate will be employed in one of the following French
research lab, depending on her/his specific profile and scientific
project:
- 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:
*
Each potential candidate is advised to contact the project coordinator
and the local coordinators of interest as soon as possible to express
her/his intent to submit an application.
*
Deadline for applications is on May 15th, for a starting date between
September 1st 2024 and December 31st 2024, to be negotiated.
*
Candidates should 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 (i) a CV, (ii) a brief research statement
(1-2 pages) & (iii) at least two contacts of reference persons (or
reference letters if available) and it should indicate the site(s) of
interest for the application.
*
The salary will depend on the successful candidate's prior research
experience and of hiring site, with a guaranteed minimum of 2300
EUR/month before taxes.
*
Each position is for a one-year post-doc.
Project summary:
RECIPROG is an ANR collaborative project (aka. PRC) running till the end
of 2025 involving french teams in Lyon, Marseille, Nantes and Marseille,
which 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, as well as software verification techniques using circular
tools.
More informations:
*
More informations can be found on the project webpage:
https://urldefense.com/v3/__https://www.irif.fr/reciprog/index__;!!IBzWLUs!VzhX9zyYRdDzMxzHaVBBvvuNMTKT_a7EkUWpFgJeHxK_X3-Bd58e4Ir0kp5xAd5rs6FVgPDcEBXFiS1FWJIW91OQJOV8TmVq_KUJWVc$ and
https://urldefense.com/v3/__https://www.irif.fr/reciprog/post-doc-offer-paril-2024__;!!IBzWLUs!VzhX9zyYRdDzMxzHaVBBvvuNMTKT_a7EkUWpFgJeHxK_X3-Bd58e4Ir0kp5xAd5rs6FVgPDcEBXFiS1FWJIW91OQJOV8TmVqq-4rZ0M$
*
Interested candidates may contact the project coordinator (Alexis
Saurin) as well as the local coordinators (Guilhem Jaber, Denis
Kuperberg, Luigi Santocanale & Alexis Saurin) to enquire about more
specific research directions and the adequacy of their research profile.
* Cross-site projects involving members of the project from different
labs are welcome.
* There is a one-year funding for each of the three sites of Lyon,
Nantes and Paris.
--
Alexis Saurin
IRIF - CNRS, Université Paris-Cité & INRIA
