From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/10619 Path: news.gmane.io!.POSTED.blaine.gmane.org!not-for-mail From: Alexis Saurin IRIF Newsgroups: gmane.comp.science.types.announce,gmane.science.mathematics.categories,gmane.comp.lang.agda,gmane.science.mathematics.logic.coq.club Subject: Post-doc position in RECIPROG project (located in Lyon, Nantes or Paris) Date: Fri, 3 Dec 2021 17:27:23 +0100 Message-ID: Mime-Version: 1.0 Content-Type: multipart/mixed; boundary="===============3538139307871372311==" Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="27621"; mail-complaints-to="usenet@ciao.gmane.io" Cc: Denis Kuperberg , Guilhem JABER To: gdr-im-JHSeY3WhOOtQFI55V6+gNQ@public.gmane.org, prooftheory.list-Re5JQEeQqe8AvxtiuMwx3w@public.gmane.org, categories-59hdLBrVOVU@public.gmane.org, types-announce-nHFbR+4dATOoZA3Q9b/B0PZ8FUJU4vz8@public.gmane.org, types-TrQ0NnR75azkdzWRgU60H7NAH6kLmebB@public.gmane.org, eutypes-Mttm5w9jbbk@public.gmane.org, GAMES-JyGdfDITRCtaq5fyzuukUWfrygkm6VTR@public.gmane.org, agda-TrQ0NnR75azkdzWRgU60H7NAH6kLmebB@public.gmane.org, coq-club-MZpvjPyXg2s@public.gmane.org Original-X-From: types-announce-bounces-0AtTguNXcGkudfPDI7pAfjevRRvlBcP1@public.gmane.org Fri Dec 03 23:02:42 2021 Return-path: Envelope-to: gcst-types-announce@m.gmane-mx.org Original-Received: from mx0a-00390e01.pphosted.com ([148.163.133.158]) by ciao.gmane.io with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) (envelope-from ) id 1mtGde-0006yk-4L for gcst-types-announce@m.gmane-mx.org; Fri, 03 Dec 2021 23:02:42 +0100 Original-Received: from pps.filterd (m0172792.ppops.net [127.0.0.1]) by mx0a-00390e01.pphosted.com (8.16.1.2/8.16.1.2) with SMTP id 1B3LS83N019875; Fri, 3 Dec 2021 17:02:01 -0500 Original-Received: from leopard.seas.upenn.edu (leopard.seas.upenn.edu [158.130.64.245]) by mx0a-00390e01.pphosted.com with ESMTP id 3cq5t3f42e-1; Fri, 03 Dec 2021 17:02:00 -0500 Original-Received: from RHIZOME.seas.upenn.edu (rhizome.seas.upenn.edu [158.130.69.24]) by leopard.seas.upenn.edu (8.15.2/8.15.2) with ESMTP id 1B3M1xpb038598; Fri, 3 Dec 2021 17:01:59 -0500 Original-Received: from RHIZOME.SEAS.UPENN.EDU (localhost.upenn.edu [127.0.0.1]) by RHIZOME.seas.upenn.edu (8.16.1/8.15.2) with ESMTP id 1B3M1xH9004789; Fri, 3 Dec 2021 17:01:59 -0500 X-Mailman-Handler: $Id: mm-handler,v 1.2 2002/04/05 19:41:09 bwarsaw Exp $ Original-Received: from mx0a-00390e01.pphosted.com (mx0a-00390e01.pphosted.com [148.163.133.158]) by RHIZOME.seas.upenn.edu (8.16.1/8.15.2) with ESMTP id 1B3GRjHB108062 for ; Fri, 3 Dec 2021 11:27:46 -0500 Original-Received: from pps.filterd (m0172792.ppops.net [127.0.0.1]) by mx0a-00390e01.pphosted.com (8.16.1.2/8.16.1.2) with SMTP id 1B3CTaR3010809 for ; Fri, 3 Dec 2021 11:27:45 -0500 Original-Received: from korolev.univ-paris7.fr (korolev.univ-paris7.fr [194.254.61.138]) by mx0a-00390e01.pphosted.com with ESMTP id 3cq5t3a5qw-1 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT) for ; Fri, 03 Dec 2021 11:27:44 -0500 Original-Received: from potemkin.univ-paris7.fr (potemkin.univ-paris7.fr [IPv6:2001:660:3301:8000::1:1]) by korolev.univ-paris7.fr (8.14.4/8.14.4/relay1/82085) with ESMTP id 1B3GRgQE002286 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-GCM-SHA384 bits=256 verify=NO) for ; Fri, 3 Dec 2021 17:27:42 +0100 Original-Received: from mailhub.math.univ-paris-diderot.fr (mailhub.math.univ-paris-diderot.fr [81.194.30.253]) by potemkin.univ-paris7.fr (8.14.4/8.14.4/relay2/82085) with ESMTP id 1B3GRgoC008694 for ; Fri, 3 Dec 2021 17:27:42 +0100 Original-Received: from mailhub.math.univ-paris-diderot.fr (localhost [127.0.0.1]) by mailhub.math.univ-paris-diderot.fr (Postfix) with ESMTP id 92740A828C for ; Fri, 3 Dec 2021 17:27:42 +0100 (CET) X-Virus-Scanned: amavisd-new at math.univ-paris-diderot.fr Original-Received: from mailhub.math.univ-paris-diderot.fr ([127.0.0.1]) by mailhub.math.univ-paris-diderot.fr (mailhub.math.univ-paris-diderot.fr [127.0.0.1]) (amavisd-new, port 10023) with ESMTP id x-9c8RIiKLgn for ; Fri, 3 Dec 2021 17:27:40 +0100 (CET) Original-Received: from mail-lj1-f174.google.com (mail-lj1-f174.google.com [209.85.208.174]) (Authenticated sender: saurin) by mailhub.math.univ-paris-diderot.fr (Postfix) with ESMTPSA id 7AA65A8270 for ; Fri, 3 Dec 2021 17:27:37 +0100 (CET) Original-Received: by mail-lj1-f174.google.com with SMTP id k2so7256064lji.4 for ; Fri, 03 Dec 2021 08:27:37 -0800 (PST) X-Gm-Message-State: AOAM530RWo+BtevUW3AeX84epyYOw+UQENWUTp+knpAyShhizXSVQhHH 3M14yta1kbWvFtzQr0kZK1jFAnyARpC6+pD8ZWo= X-Google-Smtp-Source: ABdhPJyYP7+WpXozmjaBS3qczoeLp6BHafiu5VDte29OXAU+dhH/GUyAjE5FWHP2qz8q1y4CaRo4mXtIYb9pr39TIUo= X-Received: by 2002:a2e:b058:: with SMTP id d24mr19152979ljl.237.1638548856798; Fri, 03 Dec 2021 08:27:36 -0800 (PST) X-Gmail-Original-Message-ID: X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-4.2.7 (korolev.univ-paris7.fr [IPv6:2001:660:3301:8000::1:2]); Fri, 03 Dec 2021 17:27:42 +0100 (CET) X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-4.2.7 (potemkin.univ-paris7.fr [194.254.61.141]); Fri, 03 Dec 2021 17:27:42 +0100 (CET) X-Miltered: at korolev with ID 61AA457E.006 by Joe's j-chkmail (http : // j-chkmail dot ensmp dot fr)! X-Miltered: at potemkin with ID 61AA457E.004 by Joe's j-chkmail (http : // j-chkmail dot ensmp dot fr)! X-j-chkmail-Enveloppe: 61AA457E.006 from potemkin.univ-paris7.fr/potemkin.univ-paris7.fr/null/potemkin.univ-paris7.fr/ X-j-chkmail-Enveloppe: 61AA457E.004 from mailhub.math.univ-paris-diderot.fr/mailhub.math.univ-paris-diderot.fr/null/mailhub.math.univ-paris-diderot.fr/ X-j-chkmail-Score: MSGID : 61AA457E.006 on korolev.univ-paris7.fr : j-chkmail score : . : R=. U=. O=. B=0.000 -> S=0.000 X-j-chkmail-Score: MSGID : 61AA457E.004 on potemkin.univ-paris7.fr : j-chkmail score : . : R=. U=. O=. B=0.000 -> S=0.000 X-j-chkmail-Status: Ham X-j-chkmail-Status: Ham X-Language-Detected: English X-Proofpoint-Virus-Version: vendor=baseguard engine=ICAP:2.0.205,Aquarius:18.0.790,Hydra:6.0.425,FMLib:17.11.62.513 definitions=2021-12-03_07,2021-12-02_01,2021-12-02_01 X-Proofpoint-Spam-Details: rule=outbound_notspam policy=outbound score=0 clxscore=353 suspectscore=0 lowpriorityscore=0 phishscore=0 adultscore=0 bulkscore=0 priorityscore=70 malwarescore=0 spamscore=0 impostorscore=0 mlxscore=0 mlxlogscore=999 classifier=spam adjust=-10 reason=mlx scancount=1 engine=8.12.0-2110150000 definitions=main-2112030105 domainage_hfrom=2396 X-Mailman-Approved-At: Fri, 03 Dec 2021 17:01:38 -0500 X-BeenThere: types-announce-0AtTguNXcGkudfPDI7pAfjevRRvlBcP1@public.gmane.org X-Mailman-Version: 2.1.35 Precedence: list List-Id: Announcements of interest to the TYPES community List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: types-announce-bounces-0AtTguNXcGkudfPDI7pAfjevRRvlBcP1@public.gmane.org Original-Sender: "Types-announce" X-Proofpoint-GUID: BjQlAuA9rds19htPLXxYeLPdZuCv95Eg X-Proofpoint-ORIG-GUID: BjQlAuA9rds19htPLXxYeLPdZuCv95Eg X-Language-Detected: English X-Proofpoint-Virus-Version: vendor=baseguard engine=ICAP:2.0.205,Aquarius:18.0.790,Hydra:6.0.425,FMLib:17.11.62.513 definitions=2021-12-03_11,2021-12-02_01,2021-12-02_01 X-Proofpoint-Spam-Details: rule=outbound_notspam policy=outbound score=0 clxscore=1011 suspectscore=0 lowpriorityscore=0 phishscore=0 adultscore=0 bulkscore=0 priorityscore=1501 malwarescore=0 spamscore=0 impostorscore=0 mlxscore=0 mlxlogscore=999 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.12.0-2110150000 definitions=main-2112030141 Xref: news.gmane.io gmane.comp.science.types.announce:9977 gmane.science.mathematics.categories:10619 gmane.comp.lang.agda:12814 gmane.science.mathematics.logic.coq.club:23102 Archived-At: --===============3538139307871372311== Content-Type: text/plain; charset="us-ascii" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Disposition: inline [ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] --===============3538139307871372311== Content-Type: multipart/alternative; boundary="0000000000008e829705d2406206" --0000000000008e829705d2406206 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: Quoted-printable 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 =E2=80=9C[RECIPROG post-doc appli= cation]=E2=80=9D. - 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://urldefense.com/v3/__https://www.irif.fr/reciprog/index__;!!IBzWLUs!= AJp3qP_SE47hlGSIYHOuEO7FkD-aGIJN2mM06YjRWoAzRNNywXErBF8wyEaJGzAsDAKxAGHj884= HuQ$ and https://urldefense.com/v3/__https://www.irif.fr/reciprog/post-doc-offer-dec= 2021__;!!IBzWLUs!AJp3qP_SE47hlGSIYHOuEO7FkD-aGIJN2mM06YjRWoAzRNNywXErBF8wyE= aJGzAsDAKxAGGyk0r_6g$=20 - 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=C3=A9 de Paris & INRIA --0000000000008e829705d2406206 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: Quoted-printable

This is an announcement for a postdoctoral position fu= nded 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:
- Pro= of theory
- Curry-Howard correspondence
- Logics with fixed points- Coinductive reasoning
- Proof assistants
- Type theory
- Catego= ry theory
- Automated deduction

In relation with the above= topics, an experience in one or several of the following topics will be pa= rticularly appreciated: fixed-points and circular proofs, the Coq proof ass= istant, inductive and coinductive types, guarded recursion, coalgebras, ind= uctive 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 coordinato= r: Denis Kuperberg)
- LS2N (Gallinette Team), Nantes (local coordinator:= Guilhem Jaber)
- IRIF (PPS & Picube Team), Paris (local coordinator= : Alexis Saurin)

Application process:
- Deadline for appli= cations is on January 5th 2022, for a starting date in the first trimester = of 2022, to be negotiated.
- Candidates can send their application to Al= exis Saurin (alexis dot saurin at irif dot fr) with a subject containing = =E2=80=9C[RECIPROG post-doc application]=E2=80=9D.
- The application sho= uld contain a CV, a brief research statement (1-2 pages) & at least two= contacts of reference persons (or reference letters if available).
- Th= e salary will depend on the successful candidate's prior research exper= ience with a guaranteed minimum of 2300 EUR/month before taxes.

P= roject summary
RECIPROG is an ANR collaborative project (aka. PRC) s= tarting in the fall 2021-2022 and running till the end of 2025. ReCiProg ai= ms at extending the proofs-as-programs correspondence (aka Curry-Howard cor= respondence) to recursive programs and circular proofs for logics and type = systems using induction and coinduction. The project will contribute both t= o the necessary theoretical foundations of circular proofs and to the softw= are development allowing to enhance the use of coinductive types and coindu= ctive 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 L= IRICA Team, LIS, Marseille.
- Interested candidates may contact the= project coordinator (Alexis Saurin) as well as the local coordinators (Gui= lhem Jaber, Denis Kuperberg, Luigi Santocanale & Alexis Saurin).
<= div>

--
Alexis Saurin
IRIF - CNRS, Universit=C3=A9 de Pa= ris & INRIA --0000000000008e829705d2406206-- --===============3538139307871372311==--