coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Annoucning a postdoc in Cambridge ideally suited for Coq enthusiasts

From: Timothy Griffin <tgg22 AT cam.ac.uk>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Annoucning a postdoc in Cambridge ideally suited for Coq enthusiasts
Date: Wed, 7 Apr 2021 13:23:48 +0000
Accept-language: en-GB, en-US
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=cam.ac.uk; dmarc=pass action=none header.from=cam.ac.uk; dkim=pass header.d=cam.ac.uk; arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=HVL9/RLAv8aFuQSrxSyox0XrdsaOszB0KnHC6nbEmnU=; b=M2Z1fYk/R0HmzRsqmscEKQ51dIF2wy+/7Nd1MZK68UZLJdW93L6a0plcp1voLTx4m9ZHbp0iXRkPq4+vHSyWS5mNcygZdWLQxv/6dwzm7yypm+rXAff6jKIo5QN5kySJHybX3l98cqfQ59uI+GAnj+oaeHcitB5DxoxHT9R8b/tYHEJZlGkX09cYgoNYZeMRzCJhKyoPgWRdufa9dTBDkTEoE5RAi0U0gOvHgE6MFyDwKfmZVrK9Zz0szk4Zx/+cM07GIJ2cWflvtqG9L+GwF7IYUQfhYQSKZwABtpo8uwZK4+AjN1mMnb66UjaNU+eNsyLgck4AIlrkPoBBm2eueg==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=oYHZUJBFfVCFkVlWsH52/OuGqx9QR5w/QqoD1TkD2YCvf+m9kJBbI+L0k+1tIBYH4RYC9USrQ1SzErVtX1eI3Pfd2j3dQ3vn41as2FpCFP43+WAnpZ8Zvzwto/gF7JcJcDb29klKp/aMt+YXQ/eWTExuPhna0ZCXP4KBLEh1tA6ycZbOvDMFhqGb+Fc8XCpxyje3l2bvAAZSBztMgJqwz2Krc+iglXM4r2VaAhC5NZvCDMvjqF1jsj/a2CqsvE0YQDaJHSVc/QAOq4lrEJKI2SDdfEstQWN+/0fXA4wWUBuctyxmBaDg4T2wv+BMnl8GF4dzicAwn30natkU48lCVA==
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tgg22 AT cam.ac.uk; spf=Pass smtp.mailfrom=tgg22 AT cam.ac.uk; spf=Pass smtp.helo=postmaster AT GBR01-CWL-obe.outbound.protection.outlook.com
Ironport-hdrordr: A9a23:vSCEg6lrdvXRy/GK0OTnAWtm7q3pDfPcj2dD5ilNYBxZY6WkvuiUtrAyyQL0hDENWHsphNCHP+26TWnB8INuiLN9AZ6LZyOjnGezNolt4c/ZwzPmEzDj7eI1781dWoBEIpnLAVB+5PyQ3CCRGdwt2cTC1aiui/vXwXsFd3ANV4hL6QBlBgGHVmh/QwdbDZQ0faDsn/ZvjTymZHgRc4CHFmAINtKz7uHjubDHRVo9BxAh4BSTlj/A0tLHOjWRwxt2aUIq/Z4M6m7A+jaZ2oyGk9WWjiDRzHXS6ZM+oqqo9vJmCNaXgsYYbhXA4zzYA7hJYLGJsDArrOzH0j9D/7fxii09NMd+4W65RBDXnTLR2hLt2Dtry3juxU7wuwqHneXFRSk3A8cEuIRBchGx0TtDgPhA1stwv16xht5yN1ftjS7979/HW1VBjUyvu0cvluYVkjh2TZYeQKU5l/1UwGplVLM7WA7q4oEuF+djSOvG4uxNTF+cZ3fF+kFy3d2XWGgpFBvueDlOhuWllxxt2FxpxUoRw8IS2l0a8ogmdpVC7+PYdoNlia9JVc1TSa5mHu8OTY+WBwX2MF7xGVPXBW6iOLAMOnrLpZKyyq4y/vuWdJsBy4Z3l4/GVF9eqG4ua0PjAcCDx/Rwg17waVT4eQ6o5tBV5pB/tLG5bqHsKze/RFcnlNblo/h3OLybZ9+DfLZtR9PzJ2rnHohEmyfkXYNJFHUYWMoJ/tIyW1eEpNPXOpTn39arMMr7Ff7IK3IJS2n/CnwMUHzYP8Nb9H2mXXf+nVzWQHPiekv2+JpqC6jE9+0PyIwAX7c8/TQ9uBCc3IWmODdCuqs5cA9VO7X8iJ62omGw4CLV9WlzIwFcCUxU+b3kVHtPqWYxQgDJWIdGn+/aVXFZ3XOBKBM6ctjfFxRHoU9rvYitKYaL+CwkA9W7E26TgncJvkiWR5MElqDr37amRroISrIdHI14D0HiCgF8kwcCkhY6VCY0AmvkUg7IpYrgppoOH+3bf8R7m26QULVpgEOak16dq8EpTmYcRBi0X6es8E0TbjJJm1x89LIeirKcmTCpbXAymvg8LUckUhXsPJtWSAuCf4lagbbtZUV5SnqLnyWTj1UpdnPt7Fh6vB2XEQSEPfXKCEFaoHZWz+Lj9051bHyUeytLGwVHmJw4EWTNoXBo1+CXIqK1zmuKc1MHhuUQKivMbzdXIgRgwbmMpWqosSfHEXUt3ZM1OOPBSLwlbrHIw3uobJSSirtuJY4lwL91cNT19uMbW+OWfAGYaDv+FuMywgSQ4nIoIjN9pnUome7hsSeVmlSQzTo6G77fMV5mT7YUL5WH42/oS+2B3Z95gdg21NHAQFnZe5qD0+XafjRDIhTcrSqqVOkus4lTpr93u71pHZXXOAG4pU1vzVE7NoPzm0wfSqggv+yENY9rYsAIeyVWulAuj8+CKUM3sgrwRu8yFGtd8EPzLpeM+f7Pr7FqH0iK4A33MlOb+zdG//jEUzCYvIRqeJ4YMCBTcgwk9H9m/OmebIXeBwWhavFb8DOBQwOAWa4YTLLABK4ZoRl76cyZhuObdyL33wbLoDtwS5g+jVqPUIe1GwKDGelB7ty8NxCNm8KRkbOOsAs=
Ironport-phdr: A9a23:V8rHRBxTtJwyQ8vXCzLwzVBlVkAck4WxBRYc798ds5kLTJ7L16rrMEGX3/hxlliBBdydt6sVzbOJ7Ou4ACQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagZb5+Ngi6oAfTu8UZnYduN7s6xwfUrHdPZ+lY335jK0iJnxb76Mew/Zpj/DpVtvk86cNOUrj0crohQ7BAAzsoL2465MvwtRneVgSP/WcTUn8XkhVTHQfI6gzxU4rrvSv7sup93zSaPdHzQLspVzmu87tnRRn1gyoBKjU38nzYitZogaxbvhyvugB/zYDXboGUKPVxcbjQcskGSWZdRMtdSzBNDp66YoASD+QBJ+FYr4zlqlUQrBu+AA6sBP/vyj5Im3T43Lc60+UvEQHI3QwgGc8FvXPIrNX6O6ceT/65wbLUwjrZavNawy3y55TSfhA8ovGBRLR9etfexkczDQ3KlEmQqZD7MDOP0OQAq3SX4/Z9WO+vi2AqrwB8rDeyy8oyl4TFmIMYxk3G+Ch63Is7KsO1RVJ4bNO6DJZetz+XOoV2TM0iXm1luSg3x7kAtJWmciYKz5EnyATea/yBa4WH/gjsVOOLLThimH1pYq+/hxW0/EO9yeP8TtG53VlWoiZfj9XAqnIA2wbO5sSaUPdx40ms1DWX2w3Q9+1IO104mKrfJpI7w7M9koAfvVnDEyL2gEn6kq6belkq9+Wt9ujrfq/pq56ZOoJ1lg3yLqEjltGxAeglNwUDWnWX9fm62bb+50P2Wq9KgeczkqTBsJDVO8AbpqmhDgFUz4st9wqzAyq/3NkGnXYJKktJeBWcgIf3IV3OJ+34DeukjFSrjTdrwe3JMqf5ApXXKXjDjKnucqph605dzwozy8pT55VJCrEdJPLzXUjxtN/CAhAlNAy0xv7rCNR71owARWKCGqCUPL/IvVOV+u4iIfOAaJIItDrnNvQo6f3jgWc8mVAHfKmp2ZUXaGq/HvRjO0iZfXXsgtgfHWsUpQcxUPbliFiYXTFJe3m+Rb885jIjBIK8EYjDXpytgKCG3CqjApJWYXlGBkmQHnfsaoWLQOwBaDmSI89kijwLT6KtS44n1RG0tQ/10aBrLuTO+n5QiZW2ntNy/qjYkQw43T1yFcWUlW+XBSkglWQRAjQywapXoEpny17F37Iu0NJCEtkG2/JMVRs6JNbz1e10BdH0ElbdcdjTEn6tS9DgCDp3U9FnkIxGWFp0B9j31kOL5CGtGbJAz9SjNNkP6qvZmkPJCYN4wnfC2rMmijEOScJKc2StwLN8pVG7L76MqF2QkuORTYpZ3CPJ8w+r4kC05BgdezFUFKLPUDYYe1fcqsn/6gXaVbiyBL87MwxHj8mfNq9Nbd6vhlJDFq6LEOSbWHq4niKLPTjN3qmFBKLhcmBb1S6bFUtWy2gu

Postdoc advert : https://www.jobs.cam.ac.uk/job/29323/

Closing date : 4 May 2021

---------------------------------------------------------------------------------------------------------------------------

Research Associate: £32,816 - £40,322 or Senior Research Associate: £41,526 - £52,559

Fixed-term: The funds for this post are available for 2 years.

Applications are invited for a Research Associate (PostDoc) or Senior Research Associate to focus on the working on the CAS (Combinators for Algebraic Structures) project, https://www.cl.cam.ac.uk/~tgg22/CAS.

The ideal candidate would hold a Ph.D. in Computer Science or Mathematics and have solid experience with OCaml and the Coq (pronounced like "Coke") theorem prover, although experience with other theorem provers will be acceptable.

The CAS project is using Coq to implement a language of combinators that can be used to construct complex algebraic structures for solving generalized path-finding problems. Such structures include semirings and their generalisations. The key idea of CAS is that the structures built with combinators carry proofs of their algebraic properties. Coq's extraction to OCaml is then used to build an OCaml library where the combinators produce structures with certificates of correctness.

The postdoc will be involved in all aspects of design and implementation extending an existing prototype. This will include the development of new combinators, designing Ocaml interfaces to increase usability, and developing test cases.

The CAS project was initially inspired by problems arising in the design of network routing protocols and this area of applications has motivated the current choice of combinators in CAS. However, we expect that the system will find other applications in areas such as optimisation and Operations Research.

Past funding has come from EPSRC, Cisco, and Boeing. This position will be funded with a gift from Huawei.

Further details may be obtained from Professor Tim Griffin (tgg22 AT cam.ac.uk).

[Coq-Club] Annoucning a postdoc in Cambridge ideally suited for Coq enthusiasts, Timothy Griffin, 04/07/2021