Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.


Stream: community: positions

Topic: postdoc funded by the National Research Agency


view this post on Zulip John Baez (Dec 04 2021 at 22:24):

Seen on the categories mailing list today:

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:*

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)

Application process:

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

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