Email Gateway (Oct 19 2023 at 21:11): Email Gateway (Oct 19 2023 at 21:11):From: Guillaume Burel <guillaume.burel@ensiie.fr>
Please find below an offer for a post-doctoral position near Paris. The
application date is October 31th, but the starting date can be flexible,
from 1st December 2023 up to July 2024.
Post-doctoral position in mechanized theorem proving - 12 months
Laboratory Samovar, Institut Polytechnique de Paris,
Telecom SudParis, Évry-Courcouronnes, France
(Please find the French version below)
Detailed information and candidacy here:
https://institutminestelecom.recruitee.com/l/en/o/offre-type-telecom-sudparis-type-de-contrat-duree-fh-2-40
Context
=======
This position takes place within the French ANR project ICSPA
(http://icspa.inria.fr/), which seeks to improve trust in proof
assistants based on set theory (B method, TLA+). To do this, the idea is
to export proofs found by such tools into the Dedukti logical framework,
and also to import proofs from Dedukti into these assistants. By having
the proof verified in Dedukti, we increase confidence in what the
assistant claims. In the other direction, this enables the proofs to be
certified for industrial use. Finally, by moving down from one assistant
to Dedukti and then up again to another, this enables interoperability
between them.
This position focuses on the Atelier B tool developed by Clearsy (a
member of the ANR project consortium).
Activities
==========
The candidate will be required to carry out the following tasks:
working with Clearsy to instrument the Atelier B tool in order to
recover a proof trace ;
from such trace, reconstruction of a proof in Dedukti ;
The candidate shall collaborate with all people involved in the ICSPA
project.
Job requirements
================
Experience in logic in computer science, mechanized theorem proving, and
good level in programming (if possible, using OCaml) are requested.
In addition, knowledge of a proof assistants, of the B method and/or in
automated theorem proving will be appreciated.
Application
===========
Candidates should apply online at
before October 31th, 2023.
To apply, please send us a CV, a cover letter and a summary of your
doctoral thesis.
For more information, please contact Guillaume Burel
<guillaume.burel@ensiie.fr>.
Email Gateway (Feb 16 2024 at 11:21):From: Guillaume Burel <guillaume.burel@ensiie.fr>
The following post-doctoral position has been reopened until March 5th. The starting date can be up to July. Please apply online at
https://institutminestelecom.recruitee.com/l/en/o/offre-type-telecom-sudparis-type-de-contrat-duree-fh-2-40
Do not hesitate to transfer this offer to anyone interested.
Post-doctoral position in mechanized theorem proving - 12 months
Laboratory Samovar, Institut Polytechnique de Paris,
Telecom SudParis, Évry-Courcouronnes, France
The position can take place at Évry and/or on the Paris-Saclay campus.
Detailed information and candidacy here:
https://institutminestelecom.recruitee.com/l/en/o/offre-type-telecom-sudparis-type-de-contrat-duree-fh-2-40
Context
=======
This position takes place within the French ANR project ICSPA (http://icspa.inria.fr/), which seeks to improve trust in proof assistants based on set theory (B method, TLA+). To do this, the idea is to export proofs found by such tools into the Dedukti logical framework, and also to import proofs from Dedukti into these assistants. By having the proof verified in Dedukti, we increase confidence in what the assistant claims. In the other direction, this enables the proofs to be certified for industrial use. Finally, by moving down from one assistant to Dedukti and then up again to another, this enables interoperability between them.
This position focuses on the Atelier B tool developed by Clearsy (a member of the ANR project consortium).
Activities
==========
The candidate will be required to carry out the following tasks:
The candidate shall collaborate with all people involved in the ICSPA project.
Job requirements
================
Experience in logic in computer science, mechanized theorem proving, and good level in programming (if possible, using OCaml) are requested.
In addition, knowledge of a proof assistants, of the B method and/or in automated theorem proving will be appreciated.
Application
===========
Candidates should apply online at
before March 5th, 2024.
To apply, please send us a CV, a cover letter and a summary of your doctoral thesis.
For more information, please contact Guillaume Burel <guillaume.burel@ensiie.fr>.
Last updated: Apr 28 2024 at 20:16 UTC