Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Postdoctoral position at Inria Saclay : B in Dedukti

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Postdoctoral position at Inria Saclay : B in Dedukti


Chronological Thread 
  • From: Gilles Dowek <gilles.dowek AT ens-paris-saclay.fr>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Postdoctoral position at Inria Saclay : B in Dedukti
  • Date: Thu, 24 Feb 2022 16:40:09 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gilles.dowek AT ens-paris-saclay.fr; spf=SoftFail smtp.mailfrom=gilles.dowek AT ens-paris-saclay.fr; spf=None smtp.helo=postmaster AT olive.lsv.ens-cachan.fr
  • Ironport-data: A9a23:SjTXkqvClVvlj2El5EFSmZFaSufnVLVYMUV32f8akzHdYApBsoF/q tZmKWqCM66JZDCmKo8jYYTloBlS75CDm9BgHVY/qikyRH4QgMeUXt7xwmXYb3rDdJWbJK5Ex 5xDMYeYdJhcolv0/ErF3m3J9CEkvU2wbuOgTraCY0idfCc8IMsboUsLd9UR38g52bBVPyvX4 Ymo+5eFZAf+s9JJGjt8B5yr+EsHUMva42twUmwWPZina3eD/5W9JMt3yZCZdxMUcKEMdgKJb 7qrIIWCw4/s10xF5uVJPVrMWhZirrb6ZWBig5fNMkSoqkAqSicais7XOBeAAKtao23hojx/9 DlCnZ/3GCoLb7Deo/scEEFBTgtbGZV73IaSdBBTseTLp6HHW3zowutjSkUtI8sV/P0yCmhF9 fUebj4XBvyBr7vtkPThEbAq1p1ldpW7VG8ckikIITXxAvciRZ3YBanN+tJb9Do2nYVWFOzff I8CYDFrZQWGbQcn1lI/VsJuwLz32RETdRVhqmikmpU36VKQzR1fy6HdDMffPYKFEJA9ckGw/ z6XrjupXXn2Lue3wj2ct3mom+XnhjL+QItUFbui9/csjkf7+4AIIBoSVEW25/2ilAiwQbqzN nD45AIt6vkf1h22XOLiXl7guSOumzokZv5pRrhSBB629oLY5AOQB24hRzFHacA7uMJeedDN/ gXV9+4FFQCDo5XJGS3NqOr8QSeaY3NEfTNqiTosFFNt3jX1nG0kpjz1JjqJOJC0ksfkXCrt2 XWxoSk4it3/ZuZai/njpTgrbxoHQJzECwI4oyvNV2Su42tEiGONYIip91Wd6e1eaoiDJrVgg JTms5TChAztJcjT/MBofAnqNOvyj8tpyBWG3TZS82AJrlxAOxeLJOi8Gg1WKkZzKdojcjT0e kLVsg45zMYNYCb0MfYvO9vpVJlCIU3c+TLNC6C8gj1mPMIZSeN71Ho2NSZ8IkiwyBR9wfxhU XtlWZbzUipy5VtbIMqeHrtMgOB7mUjSNEvJSJby0xm9uYdyl1bLIYrpxGCmP7BRxPrd+G39q o8PX+PXm0Q3bQEISneLqNJ7wJFjBSZTOK0aXOQNKLbYe1I+QDtJ5j246epJRrGJVp99zo/gl kxRkGcBoLYmrXGYewiMdF55b7bjAcR2oX4hZH1+MFCznmAqe4e0qbwWfJ8+bP8p7rU7n/JzS vAEfeSGA+hOE2icq2xFMMGt9YEyJg62gQ+uPja+ZGRtdZBXQQGUqMTveRHi9XVTAyfu7Zk+r rSs2xn1W50GQwg+Xs/aZOj2ngG8u2NYgOtoXlCNOdBYfEz9toZwcnSjgvgyKsAKCBPC2jrDi 13GWU9F/bmUrtZsotfThK2Co4O4KMdEHxJXTzvB8LK7FSjG5W7/k4VOZ+CFIGLGX2Tu9aT+O OhYwq2uMPADm1oW4YNwH6wxlvA549rxqvle1RoiEXPQKl+iAbNpJD+Ix5AX5KFKw7ZYvyqwW 16OqoUGYe7VZJu9HQ5DPhchY8SCyeoQxGvY48M1F1qktiV5y7qwVxkANRe7jiEAfqB+N5kow Lp7tZdOuRC/kBcjLv2PkjtQqzaXNnUFXqh75IsWBpTn1lgixl1YOMaODSv3/pzJb85SdEcwe 2fGiK3HjrVa50zDb3tjSieWjbYN3cwD6EJQ0VsPB1WVgd6b1PU56x1m7mhlRApiyBgagfl4P XJmNhArKPzWrStonsVKQ0ulBxpFWE+C4kX0xlYE/IEDo5JEioAZwKwB1eexEIQx9GZdYDUd+ KqGjmvjSnPhdcrx1y10V1QNRzkPizBu3lWqpSxlN53t81oGjf7Nj6m1IHIBsRr8RNg4j0nOt K9k5o6crIXlYDUIrfRT55ayjtwtpdPtGICGafxn5+YRFHvdY3Sp0DOKIlH3dNklyzkmN6OnI 5QGG/+jnChSGMpDQv73yELMz3JJcCYV2ec/
  • Ironport-hdrordr: A9a23:bosQ9KO3qKpZRsBcTtCjsMiBIKoaSvp037BZ7SFMoHtuA6mlfq GV7ZYmPHDP5Qr5NEtBpTniAsW9qBHnn6KdiLN5VdyftWLdyQiVxe9Zg7cKjweOJxHD
  • Ironport-phdr: A9a23:AIn49BePUPqjkLH2tZsx67cBlGM+/9fLVj580XLHo4xHfqnrxZn+J kuXvawr0AWTG9SBoK0aw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzH cBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94PNbwlSgDexf7x+I Re3oA7MqsQYnIxuJ7orxBDUuHVIYeNWxW1pJVKXgRnx49q78YBg/SpNpf8v7tZMXqrmcas2S 7xYFykmPHsu5ML3rxnDTBCA6WUaX24LjxdHGQnF7BX9Xpfsriv3s/d21SeGMcHqS70/RDKv5 LppRhD1kicKLz03/m/YhcN+kqxVoA+vqABwzYPPfIGYN+Bzcr/Bcd4UR2dMWNtaWSxbAoO7a osCF+sPPedcr4n5uVQOtga1CwerBOLh1DBIhWL90Ko10+QgFQHG2BIvH8kUvHvJq9X0OrkdU eOuwabWyzXDdOpa2S/n54jScxAhuuiAXalqfsXNzUkgDQPEgk+eqYz/Jj6Y0PkGvGeH4eR6T +2vl3InpB9rojip3sohiYbHip4bx13A9St13IQ4K9K6RUB0b9OpEZldui6HOodrQ84uX2Nlt Ds6xLMGt5O2cioHxYkoyhPDafGJc4aG7xT+X+iSOTd1nG9pdby8ihqo70StxPDwWtO33VpXt CZJjNbBu3MV2xDO5MWKSeFx8lmv1DqSzQze6fxILVo0mKbFLZMq36Q+mYAJsUvZGy/7gEX2g 7GSdkUj4uWo7ODnYrT4ppCCLYN0jhr+Mro0lsOhB+Q4KRECUHSB9uug1L3s50v5TK9Ejv0si qXZsZbaKtoHpqOhHgNY3IUu5wyhAzqozdgUh3oKIE9fdB6ZgIXkOEnCIPXiAve+h1Ssni1rx /fDPrD5DZXNL3zDkLP/crZm8UJT1Q0zzN5B6JJXEbwOPvTzWlTouNzAFBA5KQ20w/3+BNVmz IwRRWaPDbWZMa/Iv1+I/PojI++Xa4ANojbyN+Al5+LyjX8+gVIRYLGl3YELZ3CgAvRmP0KZb GLwjdcGCGcGpxYxTOj3iFKZSjNTfHazX6ck5j4hEo6mDIHDRpqsgLObxiu7EIdWNSh6DQWHF m6tfIGZUd8NbjiTK4lviG8qT7+kHqAg0RWjr0fWzKVqLaKA9SwcsZ/4ktRy+ODQvRw07nlsB t6cyCSWRmpwl3JOSSVgj/M3mlB01lrWifswuPdfD9EGv5uhMy8/PJ/YlKlhDszqHxnGZpGPQ UqnRdOvBXcwSMgwypkAeRU1AM2s2zbE2SfiGLoJj/qTHpVh/aPY23XqYcp61HvF/KQnlBw+S 9FOLii9j6V7/hmVCZSa216BmfORcqoA8ifM8C+YyHaW+kRRUQp+S6LACH8eYk/btpL14VzPT JejD69iKgJbyNXHMaJBbtT4y1tcF7/4INqLRWW3li+rAAqQgLOBaI2/Y2IGwCDUE1QJiSgU+ XeYOE46HTnnrmTFSTdnHlLmZQXi64GSsVudSUk5h0GPZkxljP+u/wINwOebU7UV164FvyEor 3N1Gky81pTYEYjIoQ0pZ6habd4nhTUPnWvEqwxwOIChJKF+lxYfdQpwpUbnyxRwDM1Jj8Erq HogyAc6J7if1RtNcDaR3Ja4PbOySCG68xGrb6PNnF3Zz9uV0qoJ87Egok/ip0SyH0Em+mQh3 cMUm3qQ65PWDRYDBIrrWxVSlVAyrLXbby8hooLMgCQ3Ye/u6WaEi4tvXrd1mXPCN59FPaiJF RH/CZgfDsmqc6kxnkSxKwkDJKZU/bI1OMWvc72H3rSqNaBuhmHD7ywP7YZj30aL7yc5RPTP2 sNPzPCc2gacETv7k1qims3xgsVcbCsTBS+kwCPgDZ8XaLc4LuNpQS++Zta6wNlzncunVH9c8 FO4QV8Bx8KqUReUdBnl1BdRzgEMqHejkDr+wSY+wFRL5uKPmSfJxerlbh8OPGVGEXJjgVnbK o+xl9kGXUKsYmDFjTOe4kjm6aFaoOw/KmDSRRwNZC3qNyR5VbP2sLOeYslJ4ZdusCNNUe36b 0rIArL6phIb1UaBVyNZyng0djWut46/kxtlhWG1IXBo6WLQY8BrgAzW79jVVLhfxHIHX2F5j zLTB16xM5G1+p2SkIum0Kj2W2+6V5JVeDXmhdrb5G3hvjQsUUT5xazj0tT8WRA3yyr6y8VnW W3ToRDwb5OqssbyeeNrc090BUPtvs9zG4VwiIw119kb3XkXgInQ/GJSyDyjd48AgOSuNTxXG W5YprydqBLo00BiMH+TkofwV3HGh9Bke8H/eWQOnCQ088FNDq6Qqr1Chyp85FSi/mezKbBwm CkQzfw25TsUmeYM7UAizyGZD6tUEU5HMC/EmhKTqsi3tqRMIX2mery5xQxwh5ryadPK6hEZQ 3v/dpo4SGV/78F7PUmK3Hrs54LMdd/LKMoarByP1gzJhOxcOdQ/jLBZ4EgvcXK4tnojxekhi BVo1pzvp4mLJVJm+6ehCwJZPDn4NIsDvyvghqFEkoOKzpiiS99/Ty4TUsKiHpfKWHoC8O7qP AGUHHggp2eHTPDBSBSH5h4upiDGCZGiMXzRKX8CiN5rTxmUIgpRmmV2FH0zzJcjFwmsyZanf UFiozsY7V7xrF1C0KphZQL6Tn+ZqQGzLzw9Q5iWKlxY9GQgrw/cY8WE7+t1EmdV+IbktAWXK 3fefA1DCWgYHEKeT1mxN6Ov7N/Nqa6VAPH7N/LUYK7LsuVVU/6Zg5y1t+kutz/eLcCTJj9vC eZ+wkNZXGs8AM3SnzweDSIN3yPLZMqGqBru4SBxos+l8fitXg/zgOnHQ7pKbYc2pU/w0fbFa bbW23sxKC4EhMJXgyaYmP5GgwJU0Xk3Py+kFbBK3cLUZITXnKIfTxsSaicocdBN87p5xQ5Vf 8jSltLy0Ld8yP8zEVZME1L7yImvYoQRLmexOUmiZg7DPamaJTDN38D8YL+tAbxWguJOshSsu DGdW0b9NzWHnjPtWlihK+ZJxC2cORVfvsm6fHMPQSD7S8n6bxSgLNJtpToywKM5wHfRKygRN yM5eEpGrrSWqy1Cw71+F2FH8nt5PLyEliKevIy6Yt4dtfpmBDgxlvoPuS9qjeEOtWcUHbovx HuBy7wm60urmeSO1Dd9BR9HqzIQwZmOoV0nIqLBsJ9JRXfD+hsJq2SWERUD4dV/WbiN8+hdz MbCkKXrJXJM6dXRqIETBszQJdnBPH0+PBnBFTjPSRMMVz+wcHrWjEhUgbec7DfGy/py4oipg 5cIRrJBARYtEegGD01+ANEYCJBzXy0p17qAkogF42H7pxDaRMxc+J7dHKH3Y72nOHOSir9KY AENyLXzINEIN4H17Edlb0FzgIXAH0e4tTFlpSlgcAJypF5TtnV4VSg40knlYwXr7mVBTZZce zY7jBA7ee039Syp+F48IlPb4iUqwhFZcTrNjDaKNSb4NqarGJpfAC79pg4/KMGgKzs=
  • Ironport-sdr: SStwKyCfXaE0cUQlRjzOt/eaBV1IbKc3dd4kpSUp/epIBEZaduJQcyMmyMdnXI+oR+oHAiqjLX OvTwMaWrrmLZWbtZonQuKIlkb0Y3iNhXJBLi9HFU34lurE/VXvQPzP2P7SWTsgVcHWM8ecXerZ S8sS7JkoKWa8jyFMOEdDAS0gAmp/do88QjkFX0EoWBPA1NH074hRhjYBFCkxV8SrmmXijV/tnX IGDVETWAv6/zUVlx0yhu1/cNEUR0cROSclrPdK1qTlfbK+CwVD29m0nAe77gxQTXzrU0TbhN/1 Yh83q8CZWmyCXiT5oWp+E4VN

Postdoctoral position at Inria Saclay : B in Dedukti

Duration: 18 months
Location: Deducteam - Inria Saclay and LMF (CNRS and ENS Paris-Saclay)
Address: 4 avenue des Sciences, Gif sur Yvette, France
Salary: 2.132,21 euros / month net (2.653 euros / month gross)

Context: The ANR project ICSPA aims at improving confidence in the
proofs built in the context of B/Event-B and TLA+ by adding formal
proofs to these systems and independently verifying these proofs with
the Logical Framework Dedukti.

Job assignments: The post-doctoral researcher will
- extend existing formalization of Set theory in Dedukti to the
  specific set theories used in Atelier B and TLA+,
- reverse engineer proof expressed in Dedukti and coming from other
provers analyze if they can be expressed in these theories, and
translate such proofs to these theories when possible,
- cooperate with other partners of the project in charge of
instrumenting Atelier B, TLA+ and the automated theorem provers used
by these systems to produce formal proofs in this formulation of Set
theory.

Applications must include a CV, a complete list of publications and a
reference letter.



  • [Coq-Club] Postdoctoral position at Inria Saclay : B in Dedukti, Gilles Dowek, 02/24/2022

Archive powered by MHonArc 2.6.19+.

Top of Page