<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
</head>
<body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
<span id="docs-internal-guid-5f9c834e-7fff-945f-c5b9-d993f54177ad" class="">
<div style="line-height: 1.38; text-align: justify; margin-top: 0pt; margin-bottom: 0pt;" class="">
<br class="">
</div>
<div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 9pt; font-family: Arial; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">We
are looking for excellent PhD candidates and postdocs to join our project on cyclic proof theory and coinductive reasoning. The positions are available in the Computer Science Department at Ben-Gurion University in Israel.</span></div>
<div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 9pt; font-family: Arial; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">This
is a joint research effort involving Ben-Gurion University, Royal Holloway University of London, and the University of Sheffield.</span></div>
<br class="">
<div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 9pt; font-family: Arial; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">The
aim of the project is to use cyclic proof theory to push forward the state-of-the-art in the formal treatment of coinduction. Another related goal of the project is to fully integrate cyclic (implicit) reasoning into current verification tools, focusing on
interactive theorem provers. </span></div>
<br class="">
<div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 9pt; font-family: Arial; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">We
invite applications for *funded PhD and postdoc positions* in the field of cyclic proof theory, coinduction and automated reasoning. Depending on background and interests of the candidates, possible research foci are: d</span><span style="font-family: Arial; font-size: 9pt; white-space: pre-wrap;" class="">eveloping
a concise logical framework for coinduction; studying structural proof theory of cyclic systems for coinduction; implementing cyclic proof machinery into modern proof assistants; improving the foundations of cyclic proofs with a focus on soundness and modular
reasoning. </span></div>
<br class="">
<div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 9pt; font-family: Arial; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">Successful
candidates are likely to have efficient communication skills in English, as well as a track record of research expertise in a subset of the following topics:</span></div>
<br class="">
<div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 9pt; font-family: Arial; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">*
Proof theory</span></div>
<div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 9pt; font-family: Arial; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">*
Inductive and coinductive reasoning</span></div>
<div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 9pt; font-family: Arial; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">*
Use of proof assistants (eg, Coq or HOL\Isabelle)</span></div>
<br class="">
<div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 9pt; font-family: Arial; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">The
positions are available immediately, start dates are flexible. Both positions include reimbursement for travel expenses to conferences and there is no teaching load. </span></div>
<br class="">
<div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 9pt; font-family: Arial; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">The
funds for the PhD position are available for 4 years. The funds for the postdoc position are available for one year in the first instance with the possibility of extension.</span></div>
<br class="">
<div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 9pt; font-family: Arial; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">The
complete application consists of the following documents, which should be sent as a single PDF file to the email address given below:</span></div>
<br class="">
<div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 9pt; font-family: Arial; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">*
CV (including list of publications)</span></div>
<div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 9pt; font-family: Arial; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">*
One-page cover letter (indicating available start date, relevant qualifications, experience, and motivation)</span></div>
<div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 9pt; font-family: Arial; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">*
Up to three letters of recommendation</span></div>
<div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 9pt; font-family: Arial; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">*
University certificates and transcripts (BSc, MSc, and Ph.D. degrees, if applicable)</span></div>
<br class="">
<div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 9pt; font-family: Arial; font-weight: 700; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">Application
deadline: October-20-2021.</span></div>
<br class="">
<div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 9pt; font-family: Arial; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">Informal
inquiries are welcome and should be directed to Dr. Liron Cohen (<a href="mailto:cliron@cs.bgu.ac.il" class="">cliron@cs.bgu.ac.il</a>).</span></div>
<br class="">
<br class="">
<br class="">
</span>
</body>
</html>