coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Guillaume Burel <guillaume.burel AT ensiie.fr>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Erratum: Post-doctoral position in mechanized theorem proving
- Date: Fri, 16 Feb 2024 14:30:00 +0100
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=guillaume.burel AT ensiie.fr; spf=Pass smtp.mailfrom=guillaume.burel AT ensiie.fr; spf=None smtp.helo=postmaster AT mail.ensiie.fr
- Ironport-data: A9a23:ZytOqq6BauyODkz6dtx6GAxRtBbDchMFZxGqfqrLsTDasY5as4F+v mcWXjjUbvvYajT9fI12Odu09UhXuMXVn4dqHQpvpSA3Zn8b8sCt6faxfh6hZXvKRiHgZBs6t JtGMoGowOQcFCK0SsKFa+C5xZVE/fjUAOC6UoYoAwgpLSd8UiAtlBl/rOAwh49skLCRDhiE0 T/Ii5S31GSNhXgsbAr414rZ8Ekz5K6r5mtB1rADTakjUGH2xyF94K03fvnZw0vQGuF8AuO8T uDf+7C1lkuxE8AFV7tJOp6iGqE7aua60Tqm0hK6aID+6vR2nRHe545gXBYqhei7vB3S9zx54 I0lWZVd0m7FNIWU8AgWe0Ew/y2TocSqUVIISJSymZX78qHIT5fj66hNMhsIZbYIwOZQI1lC2 /cmCjJKfCnW0opawJrjIgVtrsEqLc2tMYUEu3Btiz/DZRokacmSGOOXuZkBjWp23JkUdRrdT 5JxhT5HYwnBZxlGJ1IaTpgjhuqsrnT5aDxZpRSbv8Lb5kCKkVYqiuW0boK9ltqiWcdPwkW5o n364nnLXg9db+2T6iOs7Sf57gPItXqnCdNNROLQGuRRqFaU3ykYDAAcfUCqpOGwzE+4QdNWb UIOkhfCtoA3/U2vCNT7RBy5rTiKpHbwRua8DcVnyz/X9PLv8zyZIUo8QhBKVv4k890PEGlCO kCyo/vlAjlmsbuwQH2b96uJoT7aBcTzBTVbDcPjZVFVi+QPsL0OYgTzosFLPpTdszEYMTT5w jTMoS4lhrQey8ARv0lawbwlq2/8znQqZldojukyYo5DxlkgDGJCT9b4gWU3Fd4acO6koqCp5 RDoYfS24uEUFo2qnyeQWugLF7zBz6/aaG2E2wc/QMB6p2TFF5ufkWZ4vWEWyKBBbJxsRNMVS BSM5Gu9GbcKZCb0MvEnC25PI55xl/aI+SvZugD8N4YfM8chK2drDQl0aEiZw233+HXAYolhU ap3hf2EVC5AYYw+lWLeb75EgdcWKtUWmDq7qWbTlE/8j9JzpRe9FN84Dbd5RrpktfzU8FqOq Ic32gnj40w3bdASqxL/qeY7RW3m51BibXwvg50JLLywMUB9FXs/CvTc57okdsY31+5Wj+rEt DX1EENR1FO11zWNJBSoe0JTTurlfa9+inYnYg0qH1KjgEY4baiVsawwSpoQfJscztJF88Jad fc/Rpi/Mqx9cQifozU5RrvhnbNmbyWu1F6vPTL6QT0RfKxAZg3u+/3gdA3J7CAxMzeFs+o/h 5aC1QrrZ4UJaCo/LcTRadOpl0iQu1pEks1MfkL4GPthU2Syz5pLcgvf1uQWJeMIIjX9ngqq7 R6cW0oklLOcsr0L/8nsroHaiYWQSs9VPFdQRkvf5paIbRjqxHKpm9J8YbzZbALmdT3G/Yu5b r9o1ND6CvoMmWhKv6daE7pGyaEf5cPll4RFzzZLTWn6UFC2NoxOenW2/9FDlqlo9I9rvQGbX kGu+N4DHZ6rPMjjMkAaJSt7T+Cl+MwXpALv7qUOEB2n3BN0wbuJalUNHh+ujCcGEqB5Hrl4y sgcuekXyTeFtDwUDvi8gBt5yUGwP10bcqB+tpglEI7h0QUq7VdZYK3jMCz94bDRStAVMkAVP SKmu/fQjotYwm7HQWsSFGfM78VZl58hqBBH935cBlWry/7upO474w1VyhszFj9q9xRg1/lhH 0RSLGh3GPm+xChpj819QGycIQFNKxmH8EjXyVFStmnmY2S3d27KdksRBP2s+R0HzmdiYTRrx rGU52L7WzLMfsuq/C8TW1ZgmsPzX+5K6QzOt8C2LfurR6BgT2LevZavQm4Upz/MI8A73hTHr NY32tdAU/TwMCpIrpArD4Wf668rdymFA25/WtBkwrICGDDNWTO12AXWEXuLROF2G6Xo/3O7W utUHeAeczSl1S2LkCIXOr5UHZ9wg8wSxYQjfpHFGDc4loWx/xtTnrDezCzcvFMQYs5PlJ89I 7zBdjjZHW23g2BVqlD3r8JFGzSZZOcZb1f4xNKOreACFrMYkeRWaUpp+KCFj3aUFwpG/hyvo wLIYZHN/dFi0YhBm4jNEL1JIgeJdePIS+WD9T6sv+R0bd/gNdnEsyUXoALFOzt6EKQwWdMts 5iwq//ygV34uYgpX1Djm5WuE7dD4eOwVrF1NuP1NHxrojuQavTz4hcs+3GKFrIRqYlzvvKYf gqfbNe8UfU3WN0HnX1cVHV4IiYnUq/yav/tmDO5o/GyESMi6A3gLu681HrXfGpeJz4pOZr/N 1fOgMyQxOtk9aZCOBxVIMtdIc5IEAe2E+9uPdj8riKRAWSUk0uP8Omq3wYp7TbQTGKICoDm6 JbCXQLzbwm2pLqO9txCrohupVcCOR6RWwXrkp41oLaaSgxWDVLq6cwYOJQCTJxSiS3z2df2f lkhqYfk5TrVBVx5ndfUubwPnTtzwsQDPMz4JzFv8Vn8h+KeGtabGLU4nst/yy4eR9Ygpd1L7 fkT/GbxPxX3zIsBqSP/IBCkqb8P+842DU7kNawwfwIezvre7Xg3OKRdITdw
- Ironport-hdrordr: A9a23:bEuSN6FrXbxRibBVpLqE3seALOsnbusQ8zAX/mhsVBpeadyAiq mV7ZImPGzP+VQssRYb6Ku90ci7MAvhHPFOj7X5UY3SOTUO/VHYVb2KjrGC/9SDIULDH4dmvM 8KHsRD4Z/LfD9HZK3BkWqF+rgbsb26GeyT5ds2EE0GcT1X
- Ironport-phdr: A9a23:7rzMBh+OHZRh8P9uWXy2ngc9DxPPW53KNwIYoqAql6hJOvz6uci4b QqFv74w1ReJBdydt6gUzbKO8ujJYi8p39WoiDM4TNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB 89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9sK Bi6txvdutcZjYZiN6o61x/FrmdVd+hMym5kO1Gekwzg6sus+ZJo7jhdte8m+8NcXqr2eLg1Q 6ZfADo6LW4++dfltQPETQuB53scVnsZnx9VCAXb7x/0Q4n8vDLiuuVyxCeVM8v2TaspWTu59 KdkVAXoiCYcODEn9mzcl9F9g7haoBKloBx/3pLUbYSIP/dwYq/RYdUXTndHU81MVSJOH5m8Y pMMAeQPMulXoZTzqVsQoxuwBwajGOzhxyRUhnL1x6A2z/gtHR/E0QEmAtkAsG7UrNLwNKoKU O610ajIzTHHb/xMxDf97ZbHeQ08rPGRR7J/b87RwlQoGgPKk1WQqIjlPzeP2eQQtmiU8fBsW vmyi249tQ5xpiOiydkqionSh4IVy07L+T93wIYvPNC1TlNwbtG4HpVKrS6aK5d2Td04Q2Fuo Cs31rMLtJ+1ciUL1pgqxh/SZv+af4WU/B/uWumcLDN2in54Zr6xiAq+/Eakx+PzSMS630hHo zdbntXSq3wA1Rzd586aQfVz+Ueh3CyA1wHV6uxcO0A7i7bUK4Q8wr4xipocr1rMEjXql0Xxi a+abkQk+u6y6+TmeLrqvJGcN5VyhwrjMaougtSyDfk8PwUARWSW+eux2Kf+8UD9QLhGlOM6n rTHvJzCJskWpbS1DxJU34o/8RqyATmr3M4FkXQFKF9Ifg+MgpbtO1HTO/D4Eemwg06xnjdqx vHJIKXsDonLI3PeirnuZ6x95FRZyAcrzdBQ+ZZUCrYZLfL2QEDxtdjYAgUnPAyy2ObnCdR92 Z0EVWKBGK+VKKLSsVmW6eIzO+SAeYsYtTjnJ/Ul6PPil2I1lFsdcKWzw5cbdW60EuxjI0qDY HrshtkBEX0Nvgo7VOHqh0CCUT9XZ3a2Ra08+zQ7B5y8AYjYW4CtmqKO3COgE5JIYGBGEVGME Xb2eImeVfcMcjqeIsl6nTMcT7iuV5ch1Q2ytA/907drM/LY+jcEupL7yNh1++rTmAku+jxzF sSRyn2CT2VpnmwTXDI2x6B+oUllyliZy6R4gvpYFcZS5/xTSAs6O4TcnKRGDIX5XRuEddOUQ n6nRM+nCHc/VIEf2dgLNmlgGtGmhw3G0mKAHqUYk/TfC4E19qbVwn38Ycxg0XvC/KQnlFgnT 41BLzv11eZE6wHPCtuRwA2inKGwePFEtMas3GKKzG7U+VpdTBY1S6LOG3YWekrRq939oELEV b6nT7o9YUNa0cDXDKxMZ5XyiEleAu/5MYHRfmO1n26tABvOzK6WYY7CdmMG3STQTkYewEgI5 XjTDQElHW+6pn7GSjlnFFbheUTppOZjqXe/R1IxwkeAclds05K4/AUUhPHaRelAlqkctnIHr DN5VE24w8qQC9eEoF95e75AZNom/Fpd/WfQtgg7M5q7LqFvwFAEG+hul2Xp0Rg/SoBJkMxw6 Wgv0BI3M6WTllVIazKf25n0fLzRMGj7uh61OebQ3RnF3dCa971qirxwokj/vAyvCksp8ml2m 9hT3XyG45zWDQ0UGZvvW0cz/hJ+qvnUeC44r4/T0HRtN+GzvFqgk5omGeohzh+9etoZOr6eG QvaHssBBsmjbuIw2hCoYh8CIOFO5fssJcr1EpnOkKWvPetmgHenlTEesds7jx7KrnshDLSRh cVgobnQxAaMWjbigU30t8n2ndoBfjQOBi+lziOiAodNZ6p0dIJNCGG0IsTxyM8t4vylE3Ne6 lOnAEsLncGzfh/HJVPg3AlU3FkSrDqthDG1yxR5lSoor6fZ0jaEkIGAPFIXf3VGQmVvlwKmL pW1i9QTQU2lKQI0jhahzUv83KlaqeJxNSOAJCUANzizJGZkXKyqs7OEaMMa85IkvxJcV+Gka EybQLrwy/cD+xvqBHAWhDUydjXw/478gwQ/kmWWanB6sHvef8h0gxbZ/t3VA/BLjHIKQyxxi D+fAVbZXZHh8siVk5PKr+WzEWi8TJBXWSTt1oKBuW21/yVmDAa+kPa6htD8WVFrimmmi58zB HiO9k+mKoDwssbyefpqZExpGEPx54JhF4dyn5FxzJAc1H4Gh4mEqH8OkGP9K9JeisecJDIGQ T8GxcKQ4RCwgRw4aC/VgduoCzPHm5EyArvyKnkb0S888c1QXaKd7bge2DBwvkL9twXaJ/50g jYaz/Iqrn8cmeAA/gQ3nUD/SvgfG1dVOSv0mlGG9de7+e9YeWerdbGt0Uc4l827AbWqrwdHW Xf0PJk4V3wVjI03IBfX3Xv/55uxMtbNbNYXvwCRnlHKkvJYLLo8kOELhCchN3i37hhHg6Yry Bdp25+9po2OLW5gqbm4DhBvPTrwf8oP+zvpgPUWjoOM0ouoBJkkBiQTUc6iU6ezCDxL/6eCV U7GAHgmp3ycA7aaAQKP9BIssSfUC57yf3CPeCtAnI4kGUXbfR0CxlpNBnJhxNY8Bki8zcjlO i+V/xg34Vj14ltJw+NsbVzkV3vH4R2vYXEyQYSeKxxf6kdD4V3UOIqQ9LA7GSYQ5ZCnoAGXT w7TLw1VEWEEXFCFDFH/L/Gv49fH6e2RGuu5KbPHf7yPreVUU/rAy4io18Nq+DOFN8PHOXcHb bVzwk1YQXVwANjUgR0KQi0T0S/LdM+aqVGy4Gw/r8yy9ujqRBO65YaLDOg3U50n8BS3jKGfc u+I0X8ocnAFitVVlCKOkuFFjztww2l0ejKgEKoNr3vIRaPUwOpMCgIDLjl0P41O5r492Q9EP YjajMn03/h2lK1QaR8NWFr/l8WufcFPLXu6MQaNC1uKMLCPODjGhcvqe664YbBWl+RVulu+o 3zIdi2rdiTGjDTvWx21ZKtUizqHORVFpIynWhNkCGylQdT9axy2dtFtx25To/V8ljbBMmgSN iJ5ekVGo+iL7C9Wtf54HnRI8ntvKeTsc8Ox4u/DK5cb9/VxUHwcfw1y7XIhyrpYqi9eFqUdc Mr6q9dvpxerlPKOyzchXgAc8l52
- Ironport-sdr: 65cf635a_ndcEQJXC4KJCYMqIQXrjRJIDf2lCCruoP5E3oLqjXhADnQu VTRvXCjCN7WALhv1mgpMtwPXerRiAuCYntBmQNg==
Dear all,
The link to apply to the position and to get more information was erroneous. Please go to:
https://institutminestelecom.recruitee.com/l/en/o/postdocenpreuvemecanisee
Sorry for the inconvenience.
Guillaume Burel
Le 16/02/2024 à 11:20, Guillaume Burel a écrit :
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/postdocenpreuvemecanisee
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/postdocenpreuvemecanisee
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 ;
- reciprocally, import of Dedukti proofs into Atelier B.
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
https://institutminestelecom.recruitee.com/l/en/o/postdocenpreuvemecanisee
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 AT ensiie.fr>.
- [Coq-Club] Post-doctoral position in mechanized theorem proving, Guillaume Burel, 02/16/2024
- [Coq-Club] Erratum: Post-doctoral position in mechanized theorem proving, Guillaume Burel, 02/16/2024
Archive powered by MHonArc 2.6.19+.