coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Dominic Mulligan <dominic.p.mulligan AT googlemail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Interactive theorem proving internship at AWS Cambridge, UK
- Date: Wed, 28 Feb 2024 15:35:50 +0000
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=dominic.p.mulligan AT googlemail.com; spf=Pass smtp.mailfrom=dominic.p.mulligan AT googlemail.com; spf=None smtp.helo=postmaster AT mail-qt1-f171.google.com
- Ironport-data: A9a23:JWwGJ6sMLJ/w1J8ocNuu7JaYHefnVO9aMUV32f8akzHdYApBsoF/q tZmKWCAbKuLNjDwKNl3aYzj8x4DvJLWyNNqGgZqqX1kFHkbgMeUXt7xwmXYb3rDdJWbJK5Ex 5xDMYeYdJhcolv0/ErF3m3J9CEkvU2wbuOgTrSCYEidfCc8IA85kxVvhuUltYBhhNm9Emult Mj7yyHlEAbNNwVcbCRMtcpvlDs15K6u4GlC7gRnDRx2lAa2e0c9XMp3yZ6ZdCOQrrl8RoaSW +vFxbelyWLVlz9F5gSNz94X2mVTKlLjFVDmZkh+A8BOsTAezsAG6ZvXAdJHAathZ5plqPgqo DlFncTYpQ7EpcQgksxFO/VTO3kW0aGrZNYriJVw2CCe5xSuTpfi/xlhJEAnDKQJ4ulcOmhT9 qZFImwPSz3cjcvjldpXSsE07igiBMziPYdao205iD+AUq9gTpfETKHHo9Rf2V/chOgURaeYN 5dfMGQ3Kk2fOnWjOX9PYH46tOuvg3j5cjYesBSQuK4z4mfayiR+17/iNNfQc92OA85Smy50o 0qfojijXkxFb4P3JTyt8U/vvsrpnn7HCakoE7Gq8KJJnRqz7zlGYPERfQDm+KHm2xDWt8hkA 0cT428lqbU43Fe6S8H0GRy+un+N+BAGM+e8CMU/4QCJj7PIukOXXzddCDFGb9MiuYk9QjlCO kK1c83BBC1emayNRlmm/6qX9264ZSowADAITHpRJeca2OXLrIY2hxPJa99sFq+pk9H4cQ0cJ Rja/EDSYJ1D3aY2O7WHwLzRv967SnH0ouMd4wzWWie88lo8atf6Psqn7l/U6fsGJ4GcJrVgg JTms5jAhAztJcjS/MBofAnrNO/xjxpiGGCN6WOD57F7q1yQF4eLJOi8Gg1WKkZzKdojcjT0e kLVsg45zMYMZCryMP8pPNrsU59CIU3c+TLNBqC8gj1mMsgZSeN71HgzDaJt9zmxzhJ2wP5hU XtlWZ32UChDYUiY8NZGb7xAiOd0l35WKZL7Spf8wBCqmbuYbzj9dFv2GArmUwzN14vd+F+92 48HaaOikkwDOMWgOHW/2dBIdjgicyNrba0aXuQNKYZv1CI9SD9/YxIQqJt9E7FYc1N9zb6Vp CnhBhADlzISRxTvcG23V5yqU5u3Nb4XkJ7xFXZE0Y+AgiB4OdSc/+0EeoEpfLIq0uVmwLQmB 7MGYsiMSLAHADjO5z1XP9G3oZ1AZSabo1uEHxOkRzwjIL9mZQjCoeH/ciXVqSIhMyuQtOkFm YOG6D/1e5Q4aj5ZPJ7kU873l1KVlloBqd12RHrNc4Vyel2z0Y1EKB7Rr/4QIuMKI0+SwDG16 RqnPhMDgezrvYUO0cLogJqcpNyDCNpOHUt9Hkja442pNCLcwHGR/I9YXMuMfhHfTGnR+pj+Q clol9THL+wgsHNRlohNA5JH7PkZ2YP0hrl4yg9EIi36X26zAOk9HkjcjNh9iKJd45R45y6kU V2r0ftHM+yrPMjFLgYgFDA9ZL7e6cBOyyjg1tVrEkDU/yQtwaGmV39VNByyiCBwCrt5HYcm4 OU5sv4t9A2NpUs2A+mCkxxr2TyAHl4YX4Ujk6MqMovhpw4o61NFOLj3KCv95rORYNRtbGguB BKph5T5urcN/XqaLkIPFkXM09FN2rUImhRBl2EZK3qzx9Hqu/4Q3T9qywoRcDh79Bt97r9MC jBZDHEtfaSq1BV0tfdHRFGpSl1gBgXG20nfyGkptWz+TmuuXDacKmcSB/q8w0QC12d6YDJg3 aq5zVz9Wm3AZ/DB3SoVWG9kpcf8TNd3yBbwpcC/E+mBHLg4eTDAgJLyQUY18z7cHtIWqGjcg Otb7MJcSPbcC3YLgqsZD4K66+wheCqcLjYffcA7rbI7I27MXRqThx2cIF+VUeFQLaXo9USYN ZRfFvhXXU7j6BfU/yEpPo9SEbpah/Vz2cEjfInsLms4s7eyiDplnZbT1yrmjl8QXNRcvpchG 7zVag69PDSctVlMl0/Jift0CG6yTN0HRQ/7hcSe0uECEbAdu+BNL2A29JaJvEuuDQg2xCLM4 Tv/ZJLXwddylqVqvY/nSZtYCyuOdNjcaeWv8SKIiepoU+/hC8n1mj0wlkjGJCVTZLsYZMR2n ++Csfnxx0L0g4w1WGH4xbiETqlA2tquV9puIubIHWl8jwafapW9/SlZ62ScLLpXmuh8/eiif ROzM+GrRO4WWvBc5XxbUDdfGBAjEJbKbr/siCe+jvaUAD0P+FbjAPL+0lGxdkBdVCsDG6OmO z/Oo/z0u+xp9tVdNiELF9RNIsFeIma6fYAEateolz2TLlfws2O4orG4yCYRs2DaOEKlTvT/z 4nOHCXlVRKIv6rN8tFVnqpysjATD1d/meMARV0cyfEnlwGFCHM6EspFPaUkEp10lgnA5KP8b hzJb0ogDnzZdhZAehPe/t/if1m+AsojB9THHQEqrnikM3qOOIC9AbVfr3Yqpz88fzb41+ioJ O0P4nC6bFD73phtQv1V/fChx/tuwvTB3H8T5EThiIrIDg0DBakRnmlUdOaXufcrz+mW/KkKG YQ0eYyAaESySEq0CNo5PnAMR0hfszTowDElKyyIxb4zfmldIPJokJXC1yPbi9Xvr/jm4JYBQ nT4Q2aI6mGSnHcUvMPFfvo31LRsB6vj8teSdcfeqM57o010wmsgOMwGkC8GTcVk8wlae78Ye v9A/FBmbHm4xIttNHF6BOnHF1+dkp7BMt0RsDPCmA==
- Ironport-hdrordr: A9a23:uHlC5K1h5pkiYT6ns8NtTgqjBL8kLtp133Aq2lEZdPU1SL3+qy nKpp4mPHDP+VUssR0b+exoW5PgfZq/z+8W3WB5B97LNzUO01HYSb2Kg7GSpwEI2BeTygee78 pdmmRFZ+EYxGIVsfrH
- Ironport-phdr: A9a23:+rQ6iR8gnMN1xP9uWR61ngc9DxPPW53KNwIYoqAql6hJOvz6uci4b QqDur4y1ReJBdydt6gUzbKO8ujJYi8p39WoiDM4TNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB 89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9sK Bi6twrcu8sZjYZgN6o61x/FrmdVd+hMym5kO1Gekwzg6sus+ZJo7jhdte8m+8NcXqr2eLg1Q 6ZfADo6LW4++dfltQPETQuB53scVnsZnx9VCAXb7x/0Q4n8vDLiuuVyxCeVM8v2TaspWTu59 KdkVAXoiCYcODEn9mzcl9F9g7haoBKloBx/3pLUbYSIP/dwYq/RYdUXTndHU81MVSJOH5m8Y pMAAOQBM+hWrJTzqUUSohalHwagGPnixyVUinPq36A31fkqHwHc3AwnGtIDqHrarNLwNKcTV +C1zbXHxijEYfNL3Tf97InIch87rvGKQLl9dtfeyU4qFwPEiFWQqJDqMymN1ugXtmib8u5gV eaui24osQ5xpCOixsgrionOiYIVzk7L9SBjz4Y0Id20UlJ0YdmhEJZJsSyRKoR5TN84TW5yp CY61qMJuYS9fCUSyZkq2wLSZv2EfoWG/h7uSOWcLClmiX9qZL6yhwi//FS8x+PyWce5zFZHo CpEn9TQsn0D2BPe58eER/Z9/0qs2jCC3B3Q5OFcOU04i7bXJpo7zrMzlpcfq1nPEy7qlEnsk aObdFgo9+614On5ZrXmu4ScN5NqhQHkL6oum82+DvogPwQSWWWQ5P6y26f5/ULjRbVHlv02n bfdsJDdPckbo7S2Aw5R0oo68ha/Eyqq3M0WnXUaLl9JZQiLj4fuO1HJL/D4Cemwj06wnzdsw vDKJrzhApPTIXjfiLrtY6px5kpGxAcwzd1T/Y9YB7AdLP7pR0P8tsHUAgc8MwOuwubnDNt91 pkZWWKKGqKWLaTSsVqJ5uIpIumDeJUZuC7nJ/gg+v7uiXs5mV4Sfaaz25sac3+4HvNhI0WWZ XrjnNIBHn0Lvgo6VuDllFqCUTtLa3a0RK0z/is7B56+DYffWoCth6SM0DqjEp1Mem9GEkyME Wvvd4icR/gMbzuSLtZ9nTwASLiuUJQs1QqutQ//07poNPDY+iwetZL51dh6/ffflR8o9W88M 8PI2GaUCmpwg2kgRjks3ak5r1Yu5E2E1P1UhPlZE91Yr9ZUVgM7Opfah7h2DNXzXAPKOM/PT UuiRtSpCDcZQdU2zNsDZk98H5OpiRWVjHniOKMci7HeXM98yanbxXWkf66Vql7D3agl1Rw9R 9dXcHehjeh5/hTSAIjAlwOYkbyrfOISxn2F73+NmEyJukwQSwtsSePdR3lKakzTrNL47QXaC bqzDbAmPQJH4cGFLaROZ9jgjFEAT/Dma5zFe2zko26rHl6Tw6+UKo/jemETxiLYXUQDlgEV/ H3ALU47GyOlom3XChRhElXgZ07p+Oh67ni8Sxx81BmEOmtm0bf94RsJnbqcRvcUi6oDozsko i5oEUyV2tvXD5+Zu1MkcvwDOJUy51BI0W+fvAt4VnC5B4ZlgFNWMwF+vke0kg5yFp0Fi88h6 nUj0At1L6ucllJHbTKRm57qaPXRLSHp8RajZrSzuBmW2cuK+qoJ9PUzqkny9ACvGE049nx70 t5Tm3KC75TOBQAWXNr/SEEyvxR9orjbZGE66ea2nTVgNqy1tD7JncpvAfYhzhevdtF3P6SDG wv/FsQbA46lL+lr01mlYxQYPfxDobYuNpDDFbPO06qqMeB82TO+2D4fscYtjwTVqXI6E7GRj PNni7mC0wCKVinxlgKku8Hzw8VfYC0KW3C4wm7iDZJQYat7ecAKD32vKou53IYb5dalVnhG+ VqkH15D1tWufE/YY1v43AtR3gIP53m6nS+5wDVyuz4uqaWb0SnHwuCkfx0CcD0uJiEqnRL3L I64gspPFkSvagkvlRDj/QD/2qxfpat2KUHcRkBHeyXzJmBmFKC3s/DRBqwHoINtuiJRXuOmZ FmcQbOouBoW3RToGG5GzSw6fTWn0nngtyRzk3nVbHN6rX6DPNp12Q+a/tvXA/hYwjsBQiB8z zjRHFm1edezr52YkJLKs+b2UGzENNUbfS7uzIWBv22jo2h3BRm+kPm1stLgFgc+3Cry1t0sX iLN5BrxeYjk0a2mPPkvJBE5Qg+hrZMkQscnzdJV5tlY0GNSnpiP+HsbjWr/ec5W367zdjtFR DIGxcLU/Bmw3URiKnyTwIeqMxfVisBlZtS8fiYXwndnt5EMWPrSteIc23Iq+wndz0qZe/V2k zYDxOF77Xcbh7tMow8x1mCHBbtUG0BEPCvqnhDO7takrawRanz8FNr4nEd4g92lC6mP5w9GX 3OsMJslGC527845KBTJzXn3647tfvHfatUcshCRmhbEyeNSLdhi85hCzToiIm/7sXA/nqQ3i hlv25Cx+pDBLnhp+KO2CxhwOTryaMce/zjsieBVmcPcjOXNVt1xXz4MWpXvV/ehFjkf4O/mO wi5Gzo5sn6HGLDbEFzX+AJ8onnICZzuK2CPKSxT04B5XBfEbh864khcTHAgk5U+DAzv2MHxb BIz+GUK/lCh4hpUlrAzal+mAz+Z/lv3LG9zEsTXLQIKvF8eoR2OaorHsLo1R2YBr/jD5ESMM jDJOVoOVDlTHBTCXxe5ZvGv/YWSrbbeXLbvaauWJ+3J87QWVu/Ul831lNI6uW/dbIPXeSAya p9zkktbASImR4KAwWhJE2pP0HuTJ8+D+EXlon0x95/gtqStAEW1vMOOE+cAaIo0vUnn3eHbc bbX3XgcS34Q14tQlyWQmf5PgRhL0XEoL370TvwBrXKfFvuO3PIHSUdKMWUrc5IZp6MkglsXY JCd0IikkOUiyKZyUgYgNxSpjMitYYZiz3iVElTBCQ7LMb2HIWeO2MTreeamTrYWiuxIthq2s DLdEkn5Pz3FmSO7HxaoefpBii2WJnk88Mm0bwptBG7/TdnndgzzMdl5iiczyKE1gXWCPHAVM Dx1eUdA5rOK6iYQjvJ6Em1Hpn1rSIvM0z6e9PXdI40KvOFDBy11k6dD/C1/xeIKtWdLQ/t6n CaUpdlr4hmnnuSJ1jt7QU9OpzJM1+fp9Q1pPaTU8IUFWG6RpkpcqzXNTU1U/508VYS83sIYg sLCn6/yNjpYptfd/M9GQtPRNNrCKn0qdxzgBD/TCgIBCz+tL2DWwUJHw5TwvjWYqIY3rp/0l d8AULheARY5EfYbDEVuWsREJYpzWjIrmLizg8kP6n6zqRDQQINRuZWNBZfwSb3/bS2Ui7VJf U5C2bTjMYEaLZH2wWRnY1h+2Z3WQg/eBI8U5CJmaQAwrQNG9300HQhRkwr1Lwiq5nEUD/u9m BU73xB/beoa/zDp+14rJ1DOqUPYf2E+ntLqhT2UeT/1aqy3WNMPY8IVn004M5e+WhosKAPrw hUiOzDDSLZcybBncDIz4Oc5kZRIHvFYQKhNYRtWzvaSNa1A7A==
- Ironport-sdr: 65df52e3_mLRTMUMDdXu2LNZ5tjKmpLa6mvUuCxTYj0rZl8Tl1hi4jwH 2xRPqILKwX8XNKSkud2TZOvVdIyduuZa56MGS5g==
Hi,
I am hiring a 2024 intern for a position at Amazon Web Services (AWS) in Cambridge UK, working on the verification of a body of low-level code. The successful candidate will be a PhD student with existing experience in an interactive theorem proving system—ideally Isabelle/HOL, but experience in similar systems like Coq, Lean, HOL4, etc. will also be considered—and knowledge of a low-level programming language like Rust or C.
If you are interested in applying please get in touch with me directly, forwarding a CV.
Thanks,
Dominic
- [Coq-Club] Interactive theorem proving internship at AWS Cambridge, UK, Dominic Mulligan, 02/28/2024
Archive powered by MHonArc 2.6.19+.