Three Post-doc positions in RECIPROG project (located in France -- Lyon, Nantes and Paris)

--===============3757348997240931168==
Content-Type: multipart/alternative;
 boundary="=_6cfe0f6dbaf67adbdd7b57eee09956f4"

--=_6cfe0f6dbaf67adbdd7b57eee09956f4
Content-Transfer-Encoding: 8bit
Content-Type: text/plain; charset=UTF-8;
 format=flowed

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://www.irif.fr/reciprog/index and 
https://www.irif.fr/reciprog/post-doc-offer-paril-2024
  	*
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
--=_6cfe0f6dbaf67adbdd7b57eee09956f4
Content-Transfer-Encoding: quoted-printable
Content-Type: text/html; charset=UTF-8

<html><head><meta http-equiv=3D"Content-Type" content=3D"text/html; charset=
=3DUTF-8" /></head><body style=3D'font-size: 10pt; font-family: Verdana,Gen=
eva,sans-serif'>
<p><br /></p>
<p><br /><span>This is an announcement for three one-year postdoctoral posi=
tions funded by the ANR ReCiProg - Reasoning on Circular proofs for Program=
ming, to be hosted in Lyon (LIP), Nantes (LS2N, Gallinette) and Paris (IRIF=
, PPS).</span></p>
<p><br /><strong>We seek strong candidates holding a PhD in Computer Scienc=
e or Mathematics, and with expertise in one or several of the following are=
as:</strong></p>
<ul>
<li class=3D"v1level1">
<div class=3D"v1li">Proof theory</div>
</li>
<li class=3D"v1level1">
<div class=3D"v1li">Curry-Howard correspondence</div>
</li>
<li class=3D"v1level1">
<div class=3D"v1li">Logics with fixed points</div>
</li>
<li class=3D"v1level1">
<div class=3D"v1li">Coinductive reasoning</div>
</li>
<li class=3D"v1level1">
<div class=3D"v1li">Proof assistants (formalization skills or development e=
xperience)</div>
</li>
<li class=3D"v1level1">
<div class=3D"v1li">Type theory</div>
</li>
<li class=3D"v1level1">
<div class=3D"v1li">Category theory</div>
</li>
<li class=3D"v1level1">
<div class=3D"v1li">Automated deduction</div>
</li>
<li class=3D"v1level1">
<div class=3D"v1li">Automata theory</div>
</li>
</ul>
<p><span>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.=
</span></p>
<p><br /><br /><strong>The successful candidate will be employed in one of =
the following French research lab, depending on her/his specific profile an=
d scientific project:</strong></p>
<p><strong><br /></strong><span>- LIP (Plume Team), Lyon (local coordinator=
: Denis Kuperberg)</span><br /><span>- LS2N (Gallinette Team), Nantes (loca=
l coordinator: Guilhem Jaber)</span><br /><span>- IRIF (PPS &amp; Picube Te=
am), Paris (local coordinator: Alexis Saurin)</span></p>
<p><br /></p>
<p><strong>Application process:</strong></p>
<ul class=3D"v1fix-media-list-overlap">
<li class=3D"v1level1">
<div class=3D"v1li">Each potential candidate is advised to <strong>contact =
the project coordinator and the local coordinators of interest as soon as p=
ossible</strong> to express her/his intent to submit an application.</div>
</li>
<li class=3D"v1level1">
<div class=3D"v1li">Deadline for applications is on <span style=3D"text-dec=
oration: underline;"><strong>May 15th</strong></span>, for a <strong>starti=
ng date between September 1st 2024 and December 31st 2024</strong>, to be n=
egotiated.</div>
</li>
<li class=3D"v1level1">
<div class=3D"v1li">Candidates should send their application to Alexis Saur=
in (alexis dot saurin at irif dot fr) with a subject containing <strong>&ld=
quo;[RECIPROG post-doc application]&ldquo;</strong>.</div>
</li>
<li class=3D"v1level1">
<div class=3D"v1li">The application should contain <strong>(i) a CV, (ii) a=
 brief research statement (1-2 pages) &amp; (iii) at least two contacts of =
reference persons</strong> (or reference letters if available) and it shoul=
d indicate the site(s) of interest for the application.</div>
</li>
<li class=3D"v1level1">
<div class=3D"v1li">The salary will depend on the successful candidate's pr=
ior research experience and of hiring site, with a guaranteed minimum of 23=
00 EUR/month before taxes.</div>
</li>
<li class=3D"v1level1">
<div class=3D"v1li">Each position is for <strong>a one-year post-doc</stron=
g>.</div>
</li>
</ul>
<p><br /><strong>Project summary:</strong></p>
<p><span>RECIPROG is an ANR collaborative project (aka. PRC) running till t=
he end of 2025 involving french teams in Lyon, Marseille, Nantes and Marsei=
lle, which aims at extending the proofs-as-programs correspondence (aka Cur=
ry-Howard correspondence) to recursive programs and circular proofs for log=
ics and type systems using induction and coinduction. The project will cont=
ribute both to the necessary theoretical foundations of circular proofs and=
 to the software development allowing to enhance the use of coinductive typ=
es and coinductive reasoning in the Coq proof assistant, as well as softwar=
e verification techniques using circular tools.</span><br /><br /><strong>M=
ore informations:</strong></p>
<ul>
<li class=3D"v1level1">
<div class=3D"v1li">More informations can be found on the project webpage: =
<a class=3D"v1urlextern" title=3D"https://www.irif.fr/reciprog/index" href=
=3D"https://www.irif.fr/reciprog/index" target=3D"_blank" rel=3D"noopener n=
oreferrer">https://www.irif.fr/reciprog/index</a> <span>and <a href=3D"http=
s://www.irif.fr/reciprog/post-doc-offer-paril-2024" target=3D"_blank" rel=
=3D"noopener noreferrer">https://www.irif.fr/reciprog/post-doc-offer-paril-=
2024</a></span></div>
</li>
<li class=3D"v1level1">
<div class=3D"v1li">Interested candidates may contact the project coordinat=
or (Alexis Saurin) as well as the local coordinators (Guilhem Jaber, Denis =
Kuperberg, Luigi Santocanale &amp; Alexis Saurin) to enquire about more spe=
cific research directions and the adequacy of their research profile.</div>
</li>
<li class=3D"v1level1">Cross-site projects involving members of the project=
 from different labs are welcome.</li>
<li class=3D"v1level1">There is a one-year funding for each of the three si=
tes of Lyon, Nantes and Paris.</li>
</ul>
<p><br /><span>--</span><br /><span>Alexis Saurin</span><br /><span>IRIF - =
CNRS, Universit&eacute; Paris-Cit&eacute; &amp; INRIA</span></p>
<div id=3D"v1_rc_sig">&nbsp;</div>
</body></html>

--=_6cfe0f6dbaf67adbdd7b57eee09956f4--

--===============3757348997240931168==
Content-Type: text/plain; charset="us-ascii"
MIME-Version: 1.0
Content-Transfer-Encoding: 7bit
Content-Disposition: inline

_______________________________________________
Agda mailing list
[email protected]
https://lists.chalmers.se/mailman/listinfo/agda

--===============3757348997240931168==--