coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Mark Batty <mbatty AT cantab.net>
- To: acl2 AT utlists.utexas.edu, agda AT lists.chalmers.se, appsem AT lists.tcs.ifi.lmu.de, ats-lang-users AT googlegroups.com, caml-list AT inria.fr, categories AT mta.ca, cl-isabelle-users AT lists.cam.ac.uk, concurrency AT listserver.tue.nl, eutypes AT cs.ru.nl, fm-announcements AT lists.nasa.gov, folli AT folli.info, fom AT cs.nyu.edu, fstar-club AT lists.gforge.inria.fr, fun AT cs.nott.ac.uk, haskell-cafe AT haskell.org, haskell AT haskell.org, hol-info AT lists.sourceforge.net, ic.eatcs.di AT listgateway.unipi.it, idris-lang AT googlegroups.com, interval AT listserv.utep.edu, las-lics AT lists.tu-berlin.de, lean-user AT googlegroups.com, logic-list AT helsinki.fi, logic AT cs.stanford.edu, logic AT math.uni-bonn.de, loginf AT lists.tcs.ifi.lmu.de, math.logik AT gmx.net, matryoshka-devel AT lists.gforge.inria.fr, PlanetKR AT kr.org, ProofTheory AT lists.bath.ac.uk, pvs AT csl.sri.com, rewriting AT ens-lyon.fr, rewriting AT trs.css.i.nagoya-u.ac.jp, srepls AT jiscmail.ac.uk, ssreflect AT msr-inria.inria.fr, termtools AT www.lri.fr, types-announce AT lists.seas.upenn.edu, why3-club AT groupes.renater.fr, coq-club AT inria.fr, dl AT dl.kr.org
- Subject: [Coq-Club] Research Associate at the University of Kent, Canterbury, UK
- Date: Mon, 21 Aug 2023 13:41:33 +0100
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mbatty AT cantab.net; spf=Pass smtp.mailfrom=markgoespop AT googlemail.com; spf=None smtp.helo=postmaster AT mail-qv1-f49.google.com
- Ironport-data: A9a23:wynITampQNMJdyN4KliX5j3o5gxTIkRdPkR7XQ2eYbSJt1+Wr1Gzt xIaWT/TPP3fMWOmKd92b4W08B8B6pPRnYViTwI+riwxF1tH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvymTrSs1hlZHWdMUD0mhQ9oh9k3i4tphcnRKw6Ws LsemeWGULOe82Ayajt8B56r8ks156yi4mpA5DTSWNgS1LPgvylNZH4gDfrpR5fIatE8NvK3Q e/F0Ia48gvxl/v6Io7Nfh7TKyXmc5aKVeS8oiI+t5uK3nCukhcPPpMTb5LwX6v4ZwKhxLidw P0V3XC5pJxA0qfkwIzxWDEAe81y0DEvFBYq7hFTvOTKp3AqfUcAzN1cEX4nI58gpNooW30e/ McDDgw1dByM0rfeLLKTEoGAh+wmJcjveZoB4zRukWCfAvEhTpTOBa7N4Le03h9q3pEITauYP ZNIL2Y+BPjDS0Un1lM/DZskn+ivi2LndCVwp1WSqq465mHSyEp6172F3N/9JIfaGJQEzxzwS mTuzUPfOhtdLIOk4nnGy2KCvOLBhCnjR9dHfFG/3qcy3Af7KnYoIBYfUF/+pfiilmalStdHI goV/DAvpO487iSDRd7kGha8vXSspQ8ZQ9MWEusg6QjLxLC83uqCLm0NTzoEccJ/8cFqFHol0 ViGm96vDjtq2FGIdZ6D3oWJkiKsKxBLETBYeX8NdhAj3+H5rI5m23ojUe1fOKKyi9T0HxT5z DaLsDUyit0vYSgjh/XTEbfv02PEm3TZcuImzl6IAT/9v2uVcKbgNtP4swGKhRpVBN/BFgHpg ZQSpySJAAkz4XylkSWMRKAUAujs6arUdjLbhlFrEt8q8DHFF5+fkWJ4sG8WyKRBaJ5sldrVj Kn751o5CHh7YiLCUEOPS9jtY/nGNIC5fTgfatjab8BVfr96fxKd8SdlaCa4hj68yhVxz/tkZ 8bHIK5A6Er274w3nFJaoM9NgNcWKtwWmAs/uLihn0n5jeTADJJrYexabQHmgh8FAFOs+V2Jq b6zxuOFzBJQVOCWX8Uk2d97ELz+FlBiXcqeg5UPKIare1M6cEl/UaO56e16IORNwf8F/tokC 1nnBSe0PnKk1SOZQehLA1g/AI7SsWFX9C1rYH1yZQf5hBDOo++Htc8iSnf+RpF/nMQL8BK+Z 6NtlxyoU6wRGAfUsS8Qd4f8p4FEfRGmz1DGdSm8bTR1O9YqSwXV85W2NkHi5QsfPBqR7MEem ryH0h+EYJwhQw85Mt3aRsjyxHyMvF8cutlIYW32Hvdpdn7Bzq1WOg3qr/puI8gzORTJnTSb8 ACNACYnn+rGoq5r0dyQham7sJuiI9puOnVrR07gsLC8b3jc9EWe3L4aAfqpfC/cZkzw6q6Nd eVY9NCiEfwlzXJhkZtwLKZv9o06v+DQnr59yh92OVn6dHGpN+9QGWaH1sxxqaF9/L9Vlg+oU Eap+NMBG7G2FO76MVwWfiwJU/+i0KwKpzzs8vgFGkX2yytp9r6hU08JHR2tijRYHYRlIrEe3 uYtl84H2TOR0iNwHI69sRlV0GCQIlgrcaYt7MgaCbC2rDsb8AhJZJiEBxLm5J2KVc53DXArB T2q1Y7inLVXw3TQf0UjTUbt2fVvvrVQmRRo4mJbGXG3tIvkvNEV0idV0wwLdSVO7xAe0+tMK mlhbEJ0AqOV/gZXvstIXkHyOgRnBBefwEzAygYUpl3gTm2DdG/EHEsiM8mjoWEb9GN9eGBA3 be6kWzKbxfjTPvT7AATB3F3iqXEY4Rq1wvgnMuHIZy0L6Mia2C4vp70NHs6lRT3JOgQ2mvFn LBO18RtY/TZMSUwnfUKO7OC3+5NdCHedX1wetA/zqYnBmqGRSqT3wKJIEWPes9gAfzG3Eu7K s52LPJ0SBWM+3eSnw8fGJIzDed4rNwx6PoGX4HbF2oMnr+cjzhu6Zzr5nffgk0vSI5QisoTE N7aWA+DNW2yvkFqvVHxgvNKAFflXulcVjbAhLi01M4rC6M8tPpddBBu87ms4FSQHghV3zOVm wLhYaWMnupo5rpwrrToCYFGIRu+EvLodeGy6Avomc9/XdDOFsbvtg0utVjsOTpND4YRQ9hak besssb9+UH44JIabjj8oIaQMIVs/uCwbfpzHuOsC0cChgqEesvnwyVbylCCMZYTze9svJi2d TW3eO6bVIAwSdxC4FZ3diIHMRIWK5qvX5favSnn8si9UEkM4zfmcuGi22TiN1xAVykyPJb7N A/4ltCu6v1cr6VOHBU0PO5nMbApPG7cXbYaSPOpuQm6FmWIhnawionmnzck6hDJDSCKLp+rq 9aNDB3zbw+7t6z03clU+d469AEeCHFmx/I8ZAQB8tpxkCq3F3MCMf9bC5gdF5VIiWbn4fkUv t0WgLcKUk0RnAiocCkQJPzmVwabQ/UQY5L3em1v8ESTZCO7QoiHBdONM8umD2heIlPeICOPc LnyOUEc+jC+xZZmQesW7/2/x+xgw5s2A1oWrFvlnZWa7wk2WN03Ob8IIOaJfSfOFd3EngPNK HRdqaWohq2kYRaZLPuMsEK51P3UUP0DAtnogeqyLA7jhrim
- Ironport-hdrordr: A9a23:D73dEKN+u4wMGMBcTsKjsMiBIKoaSvp037BL7TEWdfU7SL37qy nDpoV56fawslYssRIb9+xoWpPwJE80nKQdieIs1PWZPTUO01HYSL2Kg7GSpAEI2BeSygee78 1dmmRFZOEYxGIUsfrH
- Ironport-phdr: A9a23:oE9KixKpMgFb/7I/A9mcuO9oWUAX0o4c3iYr45Yqw4hDbr6kt8y7e hCFu7M01Q6CAN6TwskHotKei7rnV20E7MTJm1E5W7sIaSU4j94LlRcrGs+PBB6zBvfraysnA JYKDwc9rDm0PkdPBcnxeUDZrGGs4j4OABX/Mhd+KvjoFoLIgMm7yeG/94fObwlVgDexbrN/I RurpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+V rxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs7Xims7 6BxSB/0ligIKiI3/3/LhcxxlKJXvg+qqxhwzoLIZY2YMud1cKHActMAXWdOUchRWC5BDI2yb IUBEvQPMvpDoobnu1cDtwGzCRWwCO7tzDJDm3/43bc90+QkCQzI2xYvH8gNsH/Jsdj6LrsSU fy1zaLVyjjDauhZ1i3h6IjUchEsuu2DUqh2ccrN00YgDBnJjlOOpoz5Jj6Y0PkGvGeH4eR6T +2vl3InpB9rojip3soglIbEip4Rx13F6yl03ok4KcClRENnb9OpEIZdui6aOYZqTc0vXn1kt Ds+x7MIt5O2fzUHxpo5yhLCd/CKb5WF7xT+X+ifJjd4gWhqeLO5hxuq80igzfbzVtKu3FlQs iVJiMTMtnMV2xzQ9MeHTOd98l271jmTzQzT9+JELEYpnqTYM54s2qA8moYXvEjZHSL7mF/6g LGLekgg4OSl5ODqb7P7rZGGLYB0kBvxMqE2l8y/H+s4Ng8OUnCe+eum1b3j+VT1QKxUjvEri 6XZvp/XKMABqq62BA9V1Ykj6xKhADu8zNsYmnwHIEpEeBKBkYfpJ0nDLO7kAfq7mVihkzdmy +rYMrH8BpjBNHfOnbP5cbZ48UFcyQ4zzd5F55JTD7EMOPfzVVXrtNzbAR85NBK7w/3/CNV6z oMTQm2PAqieMKPdtV+H+OcvLPONZI8RojryN/8l5/v2gX8/glASZbOp0ocPaHCkAvRmJF2Ub WT0jtcbDWgKphY+TPDtiFCaTTFcfXOyX6Yl6jE/CYKmFpvDS5u2gL2B2Se7BodZanpHClCKC 3fodp+LV+0CaCKIOsNhiCALVaC9S4890hGjrBP1y71+LubN5iIYsY/j28Nu6u3IlRAy8CR0A N6H32GMSWF0hGIISCUs0KBxu0wugmuEhKFzh6ZwCMBX5uhVSUEnKZPMxvc8BtzvHkrIcduAY FKnWcm9RzoxR9Y0zsUVJV1wX52rlgjY0i+CB74Oi6fNGJcvtKPS3j71Its7x3uCnKA9lBwiS 81AcHC9i7Rk3wfUAIHNnkqDkLuybuIX2yuJvGyKyG7LuEBDTCZxV7/EVDYRfA+ept3l60zFV b6jEpwiLgIHwsfGYqBOL9zyhF9LQPPufcnFbniqs2OxHgqTgLiFaczjcCMA32GVA08CmB0J5 3uAPhkWAia6v3nTFiJjDxTzfk6q9+064H6mUl4swhqiZFYnzafz/BpRzfKZDvoV2LUZviwsr jhyAE2V29PNF8HGoQN6deNTZs15qFlA0WbYnwJ6OpihaaFkiFlaOwpwumvlzFNxG5gGnMQ36 Dsk1xZ7M+eT1E5LXzeZxozrfLLZLXP98VaubbTX0xfQypLe9LoJwP8j7VPkoB3vH0Fk7nYjm 9lcyHiR4pGPBwMcXLrxW100+hx+4bbAbW1154rP1nBoNYG0uyTB1tYtQuw/xVLof9BbdaKCG gjaF8wBG9PoM+s3gVOkYBUeM+0U8qMoe4unfL2L0bKgJ6BsnRqijH9b74lh312F5mxhTO/Q3 tAE37XQ3wedViy5iF6nvej4nodLYTwdBG2i0TOiD4lUIuVze5oGE3mnJ+Wzx85inJP3RThF6 FO7QV4KxYvhfROJKlj81hZ40UUMvWfhhTb9xTFulzAv6KaSmGTKzu3kMQccN3RjS25lglPhL pKzksgBGkOvakxhkByq5E2/w6lAuIx/Im3IQEFLfm74LiUqVqy/t7GqaNUJ848htytQSuj6b FyHDvb5pBQb2AvmFndegi09dnSgvZP/2RB3zCqZK3lyqnTxfcBr2QyZ+NfHA/9f33wCQTQ+h TSTTl21I9nv+dKblpTrveWuEWSsStkbdCD315KHryu47ChmDAOym9i3m8b7Ck413yjh2NQsV CPSrR+6bJOvn5y+OORqYmpSLFzmrc1gFcU2qpE3g58s2XUdnIS9+XscjXy1O9xH2eT3ZzwQR npD28DOyAP+3At4NHPPzIX8Ej2Hz9R7ZsW7ZGw+1yQmqsRbD6HS4qYA1TF4vUC5sQPXbtBhh CxbwuA1rn9chegGvxskizjbC7tUH1EcdTf2mgyM9Pi8rb5cYW+udf653wxjnpTpF6qYrw9YV X3lUpI5B2px6N9+ORTN1mfy48fqYp2Ycd8JswGTlBPbp/dKN9Q1jPtMizAjcX7spXA+juc9i xtz25q3lIyGMHl2urm0CwUeKyX4YcVV9z3wye5BntfNmourA59JFS8MQYPlVrSyHTQbqfn9c QiUVHU3rW7eEr7CFyee7l1npjTBCdTjO3W/KH1fzs8kQwOSd2JFhwVBeTwgndYTHxy21YS1d U1w+iwAzlXxrAdFwKRuOgWpATSXnxuhdjphEMvXFxFR9AwXux+92a226+tyG3od5Zi9tEmWL XTdYQ1UDGYPU0jCBlb5P7Do68OTu/OACL+YKP3DKa6LtfQYT+2BkJel25d67h6HP8OTN3MkC fAniQJYRX4sI83CgH0UTjAP0SfEbsqVvhC5ryh+tMOw9/nwQAX3zYSIDLRWPNBm+hTwiqCGZ KaLnCgsDzFe29sXwGPQjrgS2FlHkyZ1azykCqgNrwbIRaPU37ZJVlsVN3I1O8xP4KYxmAJKP KY3k/vT0bh1xr4wAlZBDhn6n92xINcNOye7PU/GA0CCMPKHIyfKyof5e/H0T7oYl+hSuxCq3 FTTW0b+IjSOkSXoXBGzIKlNii+cJhlXpIC6dF5kF2HiSNvsbhDzPsVwiHU6xrg9h3WCMmB5U 3A0dklEsqGBxShRhOl2ESpH42YkZeiIliCF7vXJf44MuKgjCSB1muRGpXUinuENvWcUGbovw XqU8o89xjPu2vOCwTdmThdU/zNChYbQ+F5nJb2c7Z5YH3DN4BMK62yUTRUMvdpsTNP16MUyg pDCkrz+LDBa/pfa58wZUoLRIdiEP30sKgLuABbbCwwKSTOuPGDbwUdalbvBkx/d5oh/sZXql JcUH/VeXlUpCuIyAU1jANUIZpF6Qnl32a7eh8kO632kqRDXT8gPpZHLWMWZBvD3ISqYh71JD /cR6YvxNp9bdojy2kg5L0J/gJyPAE3IG9ZEvixmaAYw5kRL6nl3CGMpiQrpbQak4XlbEvDR/ FZ+jwJkYusq+Sz05E8fKV3Nqy89lUAwnZPuhjXZfDPqLai2VJ1bEGKu7xl3Ys69GV8kK1Hj1 UV/UVWMD6pclb5haXxmhEfHtJ1DFOQdBaxIbRkMxO2GMvAh0FBSsCKilgdM4erID4cnlRN/K 8b96SIdnVg6PZhpdP+1RuIB1FVbi6OQszX90+kwxFRbPEMR6CaJfzZOvkUUN74gLi7u/+p26 AXElSEQHQpEH/csvP9u8VswfuqayCe1mbtKMEO+MOGEN6SBk2fHksGMT1Y510dOnE5At+sTs 49rYw+PWkYjwaHEXREAL8nNLgxOd81K3HfUeimKvODEwJYzNIK4XLONL6fGpOMfhUSqGxwsF oIH45EaH5Wi50rfKN/uML8PzRh+rBSuPliOC+5FPQ6aiDpS6d/q14d5hMMOQ1NVSXU4Kyi84 azb4xMnkObWFsljeW8UB8MFLi5kA5D8wn8B+S4cU3/vlbhFgAmas22i+mKKV2K6NoQ7Iq/TP EIJapn++C1jofbozwePqNOGYTm9b4wqu8eTu71E4czbWrUEFf8l9B2E04hAGy71CSiWTZjsd sK2M851PbmWQj67SgDt1G5zFp2seo7rdu/R30npXdoG6dHLmml8aontUGlZQU44pvlftvsjP ktaMsZ9OViw8F1gUs73aAaAjof0GzfreWYQFqMPi739PuMfzjJwPLXjlj19HtdjnrPxqQlUF dkLlk2Mn6/9IdMFAG6oQDoFPFyewEhx335oMuJ4qgsm6DXPt1RUczWCdegyLXdBo8l5HlSKZ 3N/Fms/QVaYy4vF+A+lmb4IrWNbmJ5P3OtJvWKb3NeXaS+wWKGttZTesjYxJdkgraprNIX/I 8yA/JrAlz3bRZPUv0WLSim/X/Zdn9FRJmpfTpwq0Sk9PtcavINa9UcrfsI3JrgKEbd14772O HxrCikdySJfXISFnXQDjuq6x7rGh0KQfZAlY3lm+N1JhtoQVTIzYztL/vfyEdWL0TXdGy5Xc VR2j0wE/g8Lm45uc/qw5YPJSMQJ0DtKu7dvVTONEJB09lz9Q2XQgF7iSfznnfb6uGAahP/qz NQfXwZyTEZHwOMD3E4hMrJ4LKQLponSmjCPckz+sWfkye/gL15Ug56xFRWwHM/euGzwXzdJs 2UTXpNKwWrDGI46lgN4bOMyugwJLtz3PEn54DMgysJiGLzyBqXJjx416H0BQSmtCd9IDepr5 UnWVDNSaJeusJz5Op9WTwe4F7WSrFBWlEhoOi+9j5FbLpMUitbtdD1GoDHYpcXrDcMfiIl5C JgDJto5sHD4Svss0H25qHQwprXljHnU52Jk2Go=
- Ironport-sdr: 64e35b8f_WcaGBMQYWEmpEHlJsy5c91HMVutu7dYfFvZfuY79+aFlVjV DB89DnWJS31D5143IncVVzhN5lXmAx8YGn4byrw==
Apply in either of these places:
https://www.jobs.ac.uk/job/DBV331/research-associate-cems-236-23
https://jobs.kent.ac.uk/Vacancy.aspx?ref=CEMS-236-23
Salary: £36,386 to £40,931
Contract Type: Fixed Term - 36 months
https://jobs.kent.ac.uk/Vacancy.aspx?ref=CEMS-236-23
Salary: £36,386 to £40,931
Contract Type: Fixed Term - 36 months
Deadline: 4th September
The School of Computing at Kent in the UK wishes to appoint a qualified and highly motivated researcher to work as a Research Associate. This 36 month post is funded by two grants led by Professor Mark Batty (m.j.batty AT kent.ac.uk): Transparent pointer safety: Rust to Lua to OS Components from Innovate UK and Safe and secure COncurrent programming for adVancEd aRchiTectures (COVERT) from the EPSRC. This project is in partnership with Sheffield and Surrey.
Applicants should have a strong mathematical background and knowledge of how to reason about systems. This must be evidenced by high-quality research publications or artifacts in programming languages, formal verification, distributed systems, security, or computer architecture. Experience in hand proof, mechanised theorem proving tools (i.e. Isabelle/HOL, Coq, or similar) or familiarity with model checkers and SMT solvers is highly desirable.
As Research Associate you will:
1. develop formal models for the _expression_ of the behaviours of advanced architectures,
2. develop reasoning techniques (proof, mechanical proof, model checking, automated tools) for proving properties about these systems, and
3. apply these techniques to establish system properties including memory safety, security properties and functional correctness.
To be successful in this role you will:
1. have or be about to complete a PhD in a relevant discipline, or equivalent professional experience,
2. have a track record of peer-reviewed publications at scientific workshops, competitions, conferences or journals, and
3. have excellent mathematical skills relevant to analysing computer-system behaviour.
The university of Kent is walking distance from the charming historic city of Canterbury, it has a high speed connection to London, and travel to Europe is convenient by rail or car.
The School of Computing at Kent in the UK wishes to appoint a qualified and highly motivated researcher to work as a Research Associate. This 36 month post is funded by two grants led by Professor Mark Batty (m.j.batty AT kent.ac.uk): Transparent pointer safety: Rust to Lua to OS Components from Innovate UK and Safe and secure COncurrent programming for adVancEd aRchiTectures (COVERT) from the EPSRC. This project is in partnership with Sheffield and Surrey.
Applicants should have a strong mathematical background and knowledge of how to reason about systems. This must be evidenced by high-quality research publications or artifacts in programming languages, formal verification, distributed systems, security, or computer architecture. Experience in hand proof, mechanised theorem proving tools (i.e. Isabelle/HOL, Coq, or similar) or familiarity with model checkers and SMT solvers is highly desirable.
As Research Associate you will:
1. develop formal models for the _expression_ of the behaviours of advanced architectures,
2. develop reasoning techniques (proof, mechanical proof, model checking, automated tools) for proving properties about these systems, and
3. apply these techniques to establish system properties including memory safety, security properties and functional correctness.
To be successful in this role you will:
1. have or be about to complete a PhD in a relevant discipline, or equivalent professional experience,
2. have a track record of peer-reviewed publications at scientific workshops, competitions, conferences or journals, and
3. have excellent mathematical skills relevant to analysing computer-system behaviour.
The university of Kent is walking distance from the charming historic city of Canterbury, it has a high speed connection to London, and travel to Europe is convenient by rail or car.
- [Coq-Club] Research Associate at the University of Kent, Canterbury, UK, Mark Batty, 08/21/2023
Archive powered by MHonArc 2.6.19+.