PhD and Postdoctoral positions in Formal Methods for AI

--000000000000e8414e05e514f572
Content-Type: text/plain; charset="UTF-8"

The Lab for AI and Verification (laiv.uk) at Heriot-Watt University,
Edinburgh is looking to fill one PhD post and one postdoctoral post. We are
looking for candidates with solid knowledge of Theorem Proving and/or
Functional/Logic programming, and enthusiasm to apply this knowledge in the
domain of Artificial Intelligence.

The PhD post is for 4 years, starting in October 2022. It covers full
stipend and PhD fees and is sponsored by the UKRI (ukri.org) and
Schlumberger Cambridge (slb.com). The company will provide additional
training and support during the PhD studies. This post needs to be filled
in as  soon as possible.

We are also looking to employ a postdoctoral researcher for a  6-12 months
project to formalise Criminal law in the Functional Language Catala
<https://catala-lang.org/>. Formalising criminal law for autonomous cars is
of particular interest. This project will be in collaboration with Jonathan
Protzenko, Microsoft Research and the School of Law, Edinburgh University.
This project has a flexible starting date.


Please direct all queries to Ekaterina Komendantskaya ([email protected])

Best wishes,
Ekaterina

--000000000000e8414e05e514f572
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><div style=3D"font-family:Calibri,Arial,Helvetica,sans-ser=
if;font-size:12pt;color:rgb(0,0,0)"><span style=3D"color:rgb(29,28,29);font=
-family:Slack-Lato,Slack-Fractions,appleLogo,sans-serif;font-size:15px;font=
-variant-ligatures:common-ligatures">The Lab for AI and Verification (</spa=
n><span style=3D"color:rgb(29,28,29);font-family:Slack-Lato,Slack-Fractions=
,appleLogo,sans-serif;font-size:15px;font-variant-ligatures:common-ligature=
s;background-color:rgb(248,248,248)"><a href=3D"http://laiv.uk/" rel=3D"noo=
pener noreferrer" target=3D"_blank"><span style=3D"background-color:rgb(255=
,255,255)">laiv.uk</span></a></span><span style=3D"color:rgb(29,28,29);font=
-family:Slack-Lato,Slack-Fractions,appleLogo,sans-serif;font-size:15px;font=
-variant-ligatures:common-ligatures">) at Heriot-Watt University, Edinburgh=
 is looking to fill one PhD post and one postdoctoral post. We are looking =
for candidates with solid knowledge of Theorem Proving and/or Functional/Lo=
gic programming, and enthusiasm to apply this knowledge in the domain of Ar=
tificial Intelligence.</span></div><div style=3D"font-family:Calibri,Arial,=
Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)"><span style=3D"color:=
rgb(29,28,29);font-family:Slack-Lato,Slack-Fractions,appleLogo,sans-serif;f=
ont-size:15px;font-variant-ligatures:common-ligatures;background-color:rgb(=
248,248,248)"><br></span></div><div style=3D"font-family:Calibri,Arial,Helv=
etica,sans-serif;font-size:12pt;color:rgb(0,0,0)"><span style=3D"color:rgb(=
29,28,29);font-family:Slack-Lato,Slack-Fractions,appleLogo,sans-serif;font-=
size:15px;font-variant-ligatures:common-ligatures">The PhD post is for 4 ye=
ars, starting in October 2022. It covers full stipend and PhD fees and is s=
ponsored by the UKRI (</span><span style=3D"color:rgb(29,28,29);font-family=
:Slack-Lato,Slack-Fractions,appleLogo,sans-serif;font-size:15px;font-varian=
t-ligatures:common-ligatures;background-color:rgb(248,248,248)"><a href=3D"=
http://ukri.org/" rel=3D"noopener noreferrer" target=3D"_blank"><span style=
=3D"background-color:rgb(255,255,255)">ukri.org</span></a></span><span styl=
e=3D"color:rgb(29,28,29);font-family:Slack-Lato,Slack-Fractions,appleLogo,s=
ans-serif;font-size:15px;font-variant-ligatures:common-ligatures">) and=C2=
=A0<span class=3D"gmail-il">Schlumberger</span>=C2=A0Cambridge (</span><spa=
n style=3D"color:rgb(29,28,29);font-family:Slack-Lato,Slack-Fractions,apple=
Logo,sans-serif;font-size:15px;font-variant-ligatures:common-ligatures;back=
ground-color:rgb(248,248,248)"><a href=3D"http://slb.com/" rel=3D"noopener =
noreferrer" target=3D"_blank"><span style=3D"background-color:rgb(255,255,2=
55)">slb.com</span></a></span><span style=3D"color:rgb(29,28,29);font-famil=
y:Slack-Lato,Slack-Fractions,appleLogo,sans-serif;font-size:15px;font-varia=
nt-ligatures:common-ligatures">). The company will provide additional train=
ing and support during the PhD studies. This post needs to be filled in as=
=C2=A0 soon as possible.</span></div><div style=3D"font-family:Calibri,Aria=
l,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)"><span style=3D"colo=
r:rgb(29,28,29);font-family:Slack-Lato,Slack-Fractions,appleLogo,sans-serif=
;font-size:15px;font-variant-ligatures:common-ligatures"><br></span></div><=
div style=3D"font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;=
color:rgb(0,0,0)"><span style=3D"color:rgb(29,28,29);font-family:Slack-Lato=
,Slack-Fractions,appleLogo,sans-serif;font-size:15px;font-variant-ligatures=
:common-ligatures">We are also looking to employ a postdoctoral researcher =
for a=C2=A0 6-12 months project to formalise Criminal law in the Functional=
 Language <a href=3D"https://catala-lang.org/">Catala</a>. Formalising crim=
inal law for autonomous cars is of particular=C2=A0interest. This project w=
ill be in collaboration with Jonathan Protzenko, Microsoft=C2=A0Research an=
d the School of Law, Edinburgh University. This project has a flexible star=
ting date.=C2=A0</span></div><div style=3D""><br></div><div style=3D"font-f=
amily:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)"><=
span style=3D"color:rgb(29,28,29);font-family:Slack-Lato,Slack-Fractions,ap=
pleLogo,sans-serif;font-size:15px;font-variant-ligatures:common-ligatures">=
<br></span></div><div style=3D"font-family:Calibri,Arial,Helvetica,sans-ser=
if;font-size:12pt;color:rgb(0,0,0)"><span style=3D"color:rgb(29,28,29);font=
-family:Slack-Lato,Slack-Fractions,appleLogo,sans-serif;font-size:15px;font=
-variant-ligatures:common-ligatures">Please direct all queries to=C2=A0</sp=
an><span style=3D"color:rgb(29,28,29);font-family:Slack-Lato,Slack-Fraction=
s,appleLogo,sans-serif;font-size:15px;font-variant-ligatures:common-ligatur=
es">Ekaterina Komendantskaya (</span><span style=3D"color:rgb(29,28,29);fon=
t-family:Slack-Lato,Slack-Fractions,appleLogo,sans-serif;font-size:15px;fon=
t-variant-ligatures:common-ligatures"><a href=3D"mailto:[email protected]" targ=
et=3D"_blank">[email protected]</a></span><span style=3D"font-family:Slack-Lato=
,Slack-Fractions,appleLogo,sans-serif;font-size:15px;font-variant-ligatures=
:common-ligatures;background-color:rgb(248,248,248)"></span><span style=3D"=
color:rgb(29,28,29);font-family:Slack-Lato,Slack-Fractions,appleLogo,sans-s=
erif;font-size:15px;font-variant-ligatures:common-ligatures">)=C2=A0</span>=
<br></div><div style=3D"font-family:Calibri,Arial,Helvetica,sans-serif;font=
-size:12pt;color:rgb(0,0,0)"><span style=3D"color:rgb(29,28,29);font-family=
:Slack-Lato,Slack-Fractions,appleLogo,sans-serif;font-size:15px;font-varian=
t-ligatures:common-ligatures"><br></span></div><div style=3D"font-family:Ca=
libri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)"><span sty=
le=3D"color:rgb(29,28,29);font-family:Slack-Lato,Slack-Fractions,appleLogo,=
sans-serif;font-size:15px;font-variant-ligatures:common-ligatures">Best wis=
hes,</span></div><div style=3D"font-family:Calibri,Arial,Helvetica,sans-ser=
if;font-size:12pt;color:rgb(0,0,0)"><span style=3D"color:rgb(29,28,29);font=
-family:Slack-Lato,Slack-Fractions,appleLogo,sans-serif;font-size:15px;font=
-variant-ligatures:common-ligatures">Ekaterina=C2=A0</span></div><div><div =
dir=3D"ltr" class=3D"gmail_signature" data-smartmail=3D"gmail_signature"><d=
iv dir=3D"ltr"><div><div dir=3D"ltr"><div><div dir=3D"ltr"><div><div dir=3D=
"ltr"><div><div dir=3D"ltr"><div dir=3D"ltr"><div dir=3D"ltr"><div dir=3D"l=
tr"><div><div><span style=3D"letter-spacing:0.2px">=C2=A0 =C2=A0 =C2=A0 =C2=
=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=
=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0</span><br></div><di=
v><br></div><div><br></div><div><br></div></div></div></div></div></div></d=
iv></div></div></div></div></div></div></div></div></div></div>

--000000000000e8414e05e514f572--