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: Thu, 19 Oct 2023 14:57:02 +0200
Authentication-results: mail3-smtp-sop.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:bNeVBa95L+hCmdS72WQ3DrUDkHqTJUtcMsCJ2f8bNWPcYEJGY0x3n zcfUDjUOPrba2fwLtsja4Xn8U4GupXdnNFqGwVp+ytEQiMRo6IpJ/zJdxaqZ3v6wu7rFR88s Z1GMrEsCOhuExcwcz/0auCJQUFUjP3OHPymYAL9EngZbRd+Tys8gg5Ulec8g4p56fC0GArlV ena+qUzA3f7nWYvWo4ow/jb8kg25K2j4GpwUmEWPJingneOzxH5M7pEfcldH1OgKqFIE+izQ fr0zb3R1gs1KD9wYj8Nuu+TnnwiGtY+DyDW4pZlc/TKbix5m8AH+v1T2Mzwxqtgo27hc9hZk L2hvHErIOsjFvWkdO81C3G0H8ziVEHvFXCuzXWX6KSuI0P6n3TE4N9TKRpmF6YiwPdxMF9W5 PlJCQ4qV0XW7w626OrTpuhEg80iKI/mOpgeu3wmwyux4fQOGMGYBfiWo4YJgXFq35om8fX2P 6L1bRJgcRXEZxRSP1pRAo8kkeOAi3/kcjxV7lyPzUYyyzaClVwqjOO0WDbTUv6LasNeuHumn GTp4W/kHTtZN+Wa0zXQpxpAgceWwXKqB9JNfFGizdZhh0TWzWgOAjUNRF6jqL+4jFS/UpRRM SQpFjEGqKEz8AqmSML8XhD+rmTsUgMgt8R4MMcHzVrd4IHu2RefN1YcXzsQSeIBjZpjLdA17 WOhk9TsDD1plbSaT3OB67uZxQ9e3wBPcwfuggdfF2M4D8nfTJIb0kKfEos9eEKhpoepRWmhq 9yfhHJm390uYdg3O7KT02qvb9iEmJnPRQMz4AjMNo5OxlIlP9b9D2BEwfM96fsFIIvcYEOIu nMJ8/VyAcgLBJCJ0iGLW+QMEfen/Z5p0QEwY3YyQfHNFBz0qxZPmLy8Bhkkei+F1e5fIFfUj Lf741852XOqFCLCgVVLS4ywEd826qPrCM7oUPvZBvIXPMkuKlLcrHowOhHMt4wIrKTKuf9lU Xt8WZj2ZUv29Yw9k2Deqxo1je97mHhnmAs/u7ikkkj6uVZhWJJlYe5ZYQrRPr9RAFKsugjT+ spSLaO3J+Z3DoXDjt3s2d9DRXhTdCBTLcmv+6R/KLXZSiI4Qz5JNhMk6el7E2CTt/gMy7ygE 7DUchMw9WcTclWccVzQMy45MeyzNXu9xFpiVRER0Z+T8yBLSe6SAG03KPPbpJF3qrIx/u0+V PQfZcSLD9JGTzmNqXxXboDwoMYmPF6njB6HdXjtKjUuXY9SdyqQ8P/dfyzr6HYvCAizvpAAu LGO7F7QbqcCYAVAN/zoTsyT4Wm/h0VAp9IqbXD0eoFSXG7O7LlVLzfAi65rAsMUdjTG6Dio9 yeXJhY6oePLhZc8z+TUt6alrqOCMeh3LmxFFUb1sJe0Mij7+DK44IliCeynQxHUZFnWyo6DO 9pH7qjbHqUcvVBot4FcLe5a/Zgm7YGym44AnxVWInrbSn+KVJViGyCi9utSvPRvwrR5h1OHa niX8IMHBYTTadLXK39PFg8Lde/Z6Oo1nAPV5vELIEnXwi970b6EcEdKNSm3ly1vA+ppAbwh3 NselpYa2y6nhjouF+S2vCRe2mCPD34HCqscps47Bq3vgVEV0V1sW8HXJRL3x5CtUO9yFHcWD AWav4f8oohN51HjdiMzHEfd3OAGipUpvgtL/WA4JF+Iu4Tkg6Y31SJO7AYIExZc8RFD9+dBK 0lqKExHCqGc9Bh4hMV4fj6NGiMQIDa760DO218yu2mBdHaRV0vJN38YFd+W2UIkr1JnYTlQ+ Y+HxFbfUTrFeN/72g0wUxVHr8PPYMNQ9AqYvuyaBOWAQocHZAT6jp+UZWYnrwXtBeUzjhblo cho5ONBVr3pBxUPoqEUC5io6ppIcUqqfFd9ePBG+L8FOUr+ezvogDiHFB2XS/N3fvfP9Re1N txqKsdxTC+B7SeprA5KIY4XIrRxouwl28paRJPvOlw9kuW+qhhHjcvu0xbQ1U4Rbfdgq8IfE r/qVimjFzWQjEREmmWWo8hjPHG5UOY+Zwb9/b6U9dsUHMgHqNNXLEQ505qvnnCvKAA81Qmlj ADCQK73zuJZ1oVnmbX3IJhDHwmZLdDSVvyC1QKO7+R1ctLENPnRuzMvqlXIOxpcOZ0TUY9Vk YuhncHW3kSfmpoLSEHcxoe8EpdW6fWIXOZ4Ntz9KF9Yl3CgXO7u+x4yxHCqG6dWkd9y5tiVe CXgUZGeLeUqYtZ6wGFZTwN8EBxHUqT+UfrGlBOH9v+JDkAQ7BzDINaZ7kTWVGB8dBFZC62mX 0Ww87yr68tDpYtBOA4cCrs0S9VkKVvkQu09e8e3qTCcCXKyj0ifvqf50yAt8izPFmLOBfOSD UgpnfQiXE/aVGD0INBlX0hauxQWCDBwh/Ixf09b9cQeZ/VWyoIZBbx1DHnEIsg8fu/OOFXQa TfWbWovTyvnNdiBWQup+8ztB29zGcRXUuoU5VUVE4e8ZiGtBYKNRrV7nsulD7GaZRO7pNyax RoiFrEc8/R/LlyFhQre2xBjvdpa+w==
Ironport-hdrordr: A9a23:KhzHOqsHSJG9jh+19QDy+jN67skDfdV00zEX/kB9WHVpm7+j5q STdZMgpHnJYVcqKRYdcL+7VpVoLUmslqKdgrNxAV7BZmbbUQKTRekIgOffKlbbak/DH4BmpM JdmuRFaOEY0mIRsfrH
Ironport-phdr: A9a23:Va3OqhxYn8pAoKvXCzK0wFBlVkEcU1XcAAcZ59Idhq5Udez7ptK+Z hyZuqsm0QCBHd2Cra4e1ayO6+GocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wE ZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmjmwbalwI Ri3ognctssbipZmJqot1xfFuHRFd/pXyG9yOV6fgxPw7dqs8ZB+9Chdp+gv/NNaX6XgeKQ4Q 71YDDA4PG0w+cbmqxrNQxaR63UFSmkZnQZGDAbD7BHhQ5f+qTD6ufZn2CmbJsL5U7Y5Uim/4 qhxSR/ojCAHNyMl8GzSl8d9gr5XrA6nqhdixYPffYObO+dkfq7Fft0US2VOUchRWSJcHI2zc 4QBAvEdPetbtYTxu0cCoBW8CASqGejhyiVIhnjz3aAi0uohDADG3AgkH90UrXTUqcv6P7oPX OCo1qnH0zHDZO5R1Dfy9YjIcxQhofWWUrJtdMre11MjGBjYjlWKt4PlOyiY2foLs2iA7upgV Pygh3QpqwFruzWiwNonhYbViIwP0F/E6Tl5z5gvJd2+UEN2f8KoHZ9TuiyGNYZ4TM0vTm9nt Son1rALup22cSwKxpkpyRPSZPyKfouK7x/9WuicIyp0inJ7db+wmRu+7Uitx+vhXce611ZKq zBKktjKtn0VzRzc9NSISuFg/kegxTaAyR7c5vtYLkAzkKrXM58hwrgqlpoSq0vPBCH2mF/wg aSLdUsk4vCl5/njb7jovJORN4B5hhvjPqkqmsGzG/o0PhUQU2SD+umx16fv8VD7TblWlPE6j 7XVvZ/AKckVqKO0BRJe3Jw55BalFTim1cwVnXkZI1JBfxKKl43pNEvPIPD8F/uwnVKskCxqx /DHILLtGJvNLmLbnLfge7Zy9VJcxRIuwd1b6Z9YELEMLf3pVkPssNHVDgU1PxKpz+r5ENl90 5kRWWOLAq+XKqPStlqI6/ogI+mRZY8VvDL9JOI45/7rk3A1g0QSfbSz3ZQJbHC1BeppI0OCY Xrtg9cOD30GvgQkTODyjl2NSiZcZ2yuUKIk+jE7FIWmAJ/eSoy1mryOwD+7HoFKZmBBEl2DD XDod5ydV/gQbCKSP9RunycfVbmhTo8hzQuhuBX7y7phNOrU+zcXuYjt1NhvtKXvkkQ58iUxB MCA2UmMSXt1lyUGXWwYxqd69GNgy1OH2LV9jrRyCMZe47sdXRo7MZrV0ul3TdrvQA/FVtqPU 1enT5OoG2diHZoK39YSbhMlSJ2ZhRfZ0n/ya1d0v7mCBZhvt7nZw2C0PMFljXDPyKgmiVAiB MpJL2yvwKBlpEDIH4CctUKfmu6xcLgEmjbX/TKM0GuKuEhFVQM2W7jfUHQ3a03NrNX0oE3YH Pe1EbpyCgJa0oaZL7dSLNjgjFFIXvDmbdvDYma1knq1CFCC26mBaKLnfX4c3SibBlJX2xsL8 yOgMg4zTjykv3qYDDFqEgf3ZFjw9OBltH6hZko9zgXMYkt61ru4vBAP7RCFY9UU2L9M+CIoq jEvWU24w8qTEN2Y4QxoYKRbZ9o5plZBz2PQ8QJnbNSmKOh5i1gSfh4S3Qum3ghrCohGjckhr W87hAt0J6WC1VpddjSelZnuM7zTI2P28VihcanTkl3Z1d+X/O8I5pFa4x3soQCtEkM/9ngh2 cRP3n+065PRDQsfF5zrEw42+xV8u7DGc3wl/YqHsB8keaKwszLEx5coHL58m03mIosZafLZU lWrSZ5/ZYDmMuEhllm3YwhROelT8PVxJMa6b76d37btOu98nTWghGAB4YZn00vK+TAvL4yAl 5sD3fyc2ROKEjnmi1L0+M/qmIRAbCwXEyy11DLpAKZcYLZzfItNB33kcKjVjp1uwoXgXXJV7 gvpCE4H3MugZB+fKVbgxwBU/UkRun2mlG221XYn9lNh5rra1yvIzeP4cRMBMWMeX2hug2DnJ o2shswbVkylB+QwvCOs/l2yh61SpaAkanLWXV8NZC/uaWdrTqq3sLOGJc9J8pIh9ytNAqywZ lWTS7i1pBV/sWurEHZfwDQyajSn/J/khRF+oG+bN3dyoTzXY4l8yAze69rVWfNKlmNXH28l1 X+OVwX6ZYDztdyP8vWL+vizTWegSoFefWHwwIWMuTH6rWxmDBujnuyiz9juEAw0yyj+hLwIH W3DqBfxZJWu1rzvaLM8OBQ0QgattowgQ9st9+l4zIsd0nUbmJiPqH8OkGOodM5exbq7d30VA zgC39/S5gHhnkxlNHOAgYzjBRD/ioNsYce3ZmQO12cz9cdPXe2b8b1AmSJop1f+px/LbPxVk zEGyPojrnAAybJs2kJl3mCGD7YeEFMNdyPxlhCM5s27oeNdeXyidZC90lF/nN3nAqvI8WQ+E D7pP5wlGyF39MB2NlnBhWby5o/Tc97VddsPtxeQnkSIn61PJZk2jPZPmTt/NDe3oyg+0+Bix 08Lv9nyrM2dJm5q5q78HhNIKmi/eZYI4j+0xadGwpTPjtvpQ8knQ2RWGsGxF7XzSnoXpbzxP gKKWlXQs1+9HrzSVU+a4UZi9DfUFoyzcmqQPD8fxMljQx+UIApehhoVVXM0hMxxEAfi38Hnf Epjg1JZrlflthtBzP5pPBjjQy/eogmvcDI9VJmYKlJf8AhD407fNcHW4Ph0GmlU+ZiorQrFL WL+BUwAFWYSRkmNHEzuJJGr7NjEteWeHeu/Ir3Ae/TGqOBTUeuJ2YP60oZi+GXpVI3HNX1jA vsnn0tbCCkoQIKEx3NWGnFRzXuXPKv57F+m9yZ6r96y6qHuUQPrvs6UDqdKdM5o41awiLuCM OiZgGB4LyxZ39UC3yytqvBX0VgMhiVpbzToH64HsHuHQ7/RnqteEhsWLSluLsZMx686xQhMN IjVkJmms9wwxu5wEFpDWVH7z4uxYtcWJmimKF7dLEOCNbDAKDvQwsD6J62mA+417q0cp1i7v jCVFFXmNzKImmzyVhyhBupLiTmSIB1UvIzVmvlFBG74TdPrLBOhYoYfZdgezLsvh3LHc2AGY 2AUm6Jlq7SR6WVVhO5+GmEH4GA3dYG5
Ironport-sdr: 6531279c_s0jNRhx8IqJjzRlYB3VA46a5rYcb8GupMAOM2hbrRaLBXlh ZjNktPKt2BUb6YmbPLpU15oTtqTKMnyNzq1xgZw==

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 ;
- 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 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 AT ensiie.fr>.

[Coq-Club] Post-doctoral position in mechanized theorem proving, Guillaume Burel, 10/19/2023