coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Post-doctoral position in mechanized theorem proving

From: Guillaume Burel <guillaume.burel AT ensiie.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] Post-doctoral position in mechanized theorem proving
Date: Fri, 16 Feb 2024 11:20:21 +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:RY4Ma68GGUxllZA+pIRBDrUDr3qTJUtcMsCJ2f8bNWPcYEJGY0x3m 2RODGzQPa2KMWfyKtpzPY+2pBxQu5/VyoJiTAc4pHtEQiMRo6IpJ/zJdxaqZ3v6wu7rFR88s Z1GMrEsCOhuExcwcz/0auCJQUFUjP3OHPymYAL9EngZbRd+Tys8gg5Ulec8g4p56fC0GArlV ena+qUzA3f7nWYqWo4ow/jb8k835q2s4GpwUmEWPJingneOzxH5M7pEfcldH1OgKqFIE+izQ fr0zb3R1gs1KD9wYj8Nuu+TnnwiGtY+DyDW4pZlc/TKbix5m8AH+v1T2Mzwxqtgo27hc9hZk L2hvHErIOsjFvWkdO81C3G0H8ziVEHvFXCuzXWX6KSuI0P6n3TE5u5lT3NuA6YhpKUoGDARz qFfbxVSR0XW7w626OrTpuhEg80iKI/mOpgeu3wmwyux4fQOGMGYBfiWo4YJgXFq35om8fX2P 6L1bRJgcRXEZxRSP1pRAo8kkeOAi3/kcjxV7lyPzUYyyzGOllYhjOOybrI5fPSMVch6hBebo ljqxGXEOA0IH9yy0SSspyfEaujnxH+qCd1CS9VU7MVCi1qKg2cXFRc+Tkq+ufD/i0ikWtsZJ VZ8x8Y1ha079UjtQ9/mXhy15nCe1vIBZzZOO8gh40K/kpT/2ljaWXFVEQUcL5sD6+ZjEFTGy WS1t9/uADVutpicRnSc6qqYoFuO1c49dzZqicgsF1tt3jXznLzfmC4jWf5NKsaIYjDdHDjxx 3aHqjM/hrhVg9RjO0SHEbLv3mLESnvhF1NdCuDrsoSNtFoRiGmNPdzA1LQjxawcRLt1t3HY1 JT+p+CQ7foVEbaGnzGXTeMGEdmBvqndYGWG2A4wRsJxp1xBHkJPm6gNsFmSw283aK45lcPBO xCO0e+szMYLYSX1M/8fj3yZUZ9wk8AM6ugJptiNMosfPcguHON21DtjY0eM0nqFraTfuf9XB HtvSu71VSxyIf0+lFKeHr5NuYLHMwhjnAs/s7iglE/5uVdfDVbIIYo43KymMrpjtf/Z+1yIm zudXuPToyhivCTFSnG/2eYuwZoidxDX3Lin9ZYFRf3JOQd8BmAqBtnYxL5rKcQvnL1Ymq2Mt juxU1NRggi3z3DWCxS4WlY6YpPWXLF7sS0aOw4oNg2WwHQNW9ukw5oeUJoVRoMZ0tJf48R6d NQ7XvmRI+9uT23H8gsNbJOmo41Fcg+qtD20PCGkQWYeesdgTjPW5+3bIxnmyy0KKi+FpOo/v LyS+QfJSrUTRwlZLZj3adD+63iTrHQiiOZJcE+QGeZqeWLo65pPBxXqq/0Kf/E3NhTIwwWF2 zasARs3offHp6k3+oLrgZ+ogpiIEewkOGZnBEjesKiLMBfF8lqZwYNvVPiCeRbfXjjW/ISgf eBk8OHuAsYYnVpls5tOLJgz9PgQv+DQnr59yhhoOF7pbF7xU7NpHSSg7Pl176ZIwudUhBuyV kex4eJlALSuOv7+MVsvNQEgP/Wi1/YVp2Ho1s4LAn7GvQ15wLnWdn9pHUioqDdcJ75LIo8a0 b8fmMoJ2Tee1DsuEPi71x5xyUrdAEAEYasdsrMiPLTKkSsuk1FLXozdAHT54baJcNR9DXMpK T612ovHualXnE7aQUFuEHPM/PF8gK4Ws0tg124yJFWum/vEiMQo3RZXzy8FcwRNwjhD0MNxI mJONXApFZ6R/jxtutdPb1qsFy5FGhed3E77kHkNq0H0UGiqUTbrAFAmGOPQ4n0czX1QTgJb8 J6c1mzhdzTgJ+P1/ykqXH9au+7RdsNw+iLCifKYMZy8RbdiWgXcg4iqeWYsgDnkC5lohET4+ M9bzNwpYqj/bSMts6k3DreB7ospSTeGGXdjRM9w96ZYDEDefzCPgQK1EX6TQf8UBfL28h6fM fdMd+ZvTBW10Ricog8LXZAsJ6BGp993xd4gVI6yG0s4neq+lBRLvqjU1BDCv04wYtA3kc8CO oLbLD2DNWqLhEproWzGregaG2+GfNJeYBXO572w++QoDLMGivlnKmsp44u3vlKUEQppxA2Vt wX9fJ3rz/Ru5IBvvon0GIBBOlmEEszyX+G27wyDidRCQtfRO8PotQlOiF3YEylJHLkWAfJbq K+stYPp4Ub7o7oGaWDVtJ2fHa1v58/pfu52MNryHUZKjxm5R87gzBsSyV+WcaUTvotm2fCmY A+kZO+bV90fAY5dzUIITRluKU8WDqCvY5rwoS+4ke+3NSEc9g76N/Kiy27iaDBKVy0POqCmM DTOhdSV2ol6orhPVTg+PNM3M68gdRWnEeEjesbqvDaVMniwjxnQ8vH+nB4n8nfQBmPCDM/+5 onfSwPjcAip/pvF18xdr5c4qyh/4KyRWgXsVhl1Fx9KZzGG4KouKO0cNdMLDIpVkyG02ouQi PQhqoc9IX2VYNiGWUyUDBffssO3C+oVO9b0YDIzl69RQznjH5uOWdON6Q85i0qbuVLfICWPJ NcF+3z9eBarqn2sqSD/+dTj6dpaKjjmKr7kNKwzfwEew/rTPFnS6EFcIQ==
Ironport-hdrordr: A9a23:cJgFzqw10PKgsQ6X/ZRsKrPwOb1zdoMgy1knxilNoHtuA6ulfq GV7ZAmPHDP5wr5NEtPpTniAtjkfZq/z+8W3WB5B97LN2SLhILCFuFfBOXZogEIVxeOldK1Cp 0LT5RD
Ironport-phdr: A9a23:/VkuCBddJXCiKwFhNmm/JLrslGM+5NTLVj580XLHo4xHfqnrxZn+J kuXvawr0AWYG9+BoKsdw6qO6ua8AzxGuc7A+Fk5M7VyFDY9yv8q1zQ6B8CEDUCpZNXLVAcdW Pp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9Kev6AJPdgNqq3O6u5ZLTfx9IhD2gar9uM Rm6twrcutcSjId4NKo91BTFrmZVd+9LwW9kOU+fkwzz68uu/5Nv6Thct+4k+8VdTaj0YqM0Q KBXAzghL207/srnuwXdQwCS/HUcSGIWkhRJAwjB8h73W4r6vzX5uORgxiSUJNX6Qr8oVzus6 adrUwLohzwcNzEl6mHXi9d/g7xdrRm8uhFw2Y/UYIWSNPpjYqPQeM4RSGRdUspNUSFKH4WxZ JYNAeUcJ+ZVt4fzqVsQoxWjCwaiB+zgxSNHiHLtwa06yuEhHR3a0AE6Hd8DtmnfotXvNKcVV OC41KjGzSjCb/NS3Tfy8pXIchU/rvqRQL9wbNDRxlcrFwjYiViQppHlPzKR1uQJqWeb8u9gW vy1h2E8tgFxuCagxsM3h4bXgIIV0VHE9SRnz4ovK924Uld2bNi5G5Rfqy+ULZF5Qt8+Q252o iY6zKULtJ61ciQXx5oqxxHRZfKbfoWM/x7uVfucLDRmiX94Zr6zmxe//EiuxOHgWMS53ktGo zZZntXRtX0A1R3e58eZR/Z740yv1zGP1wXJ5eFFJ0A5jbDbJIA9zb4qi5oTsFjDETHol0nsk KCWcUAk9vCp6+TheLXmp4WTO5V6igHkNKklh8+xAfwgPwQTW2WW9/6w2b3s8EHjXblHiv07n rPHvJzHO8gXvqy0Dg1P3oo99xqyDy2q3dQWkHUdKF9Ifg+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/VxUHwcfwNy5X07z/1Y6jpFRfEzl jGA9raGTHmrlPKOyzchXgAc8152
Ironport-sdr: 65cf36ea_MdKXe5YOTBUPHwGzHN3W4SEwk7SBR7JAq/NhJB+rr7PVsN4 ZskqplG9tt1bWgc8P/jMoj+dunag3KwjyLoOoRw==

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:

- 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/offre-type-telecom-sudparis-type-de-contrat-duree-fh-2-40

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