<div dir="ltr"><div class="gmail_default" style="font-size:small"><div class="gmail_default" style="font-size:small">Applications are 
invited for a one-year <span><span><span>postdoctoral</span></span></span> position at the <span><span><span>University</span></span></span> of 
<span><span><span>Minnesota</span></span></span>. The position is available 
immediately; applications will be reviewed as they are 
received. <br><br>The project within which the appointment is to be made
 concerns the development of a framework that supports the encoding of 
rule-based relational specifications and the process of reasoning about 
such specifications through the encoding. An emphasis in the project is the use of the so-called higher-order abstract 
syntax approach to representing objects that embody a binding structure.
In recent work, we have developed <a href="https://arxiv.org/abs/2107.00111" target="_blank">a new logic</a> for articulating properties of LF specifications, which has provided the basis for a proof assistant called <a href="http://adelfa.cs.umn.edu" target="_blank">Adelfa</a>
 for reasoning about such properties. In other work, we are developing 
the capability to reason about linear logic specifications within the <a href="https://abella-prover.org/" target="_blank">Abella proof assistant</a> and are also using this system to explore the benefits of higher-order 
representations of syntax in the verification of compilers and 
transformers for functional programming languages. The successful candidate will be expected to 
participate in and help lead the work in some of these directions. <br><br>To
 be suitable for the position, the candidate should be broadly 
conversant with the areas of computational logic and programming 
languages and should have the mathematical and programming skills 
necessary for conducting research in them. Some particular facets that 
would
 be helpful in engaging immediately with the research problems are a prior 
exposure to a proof assistant or logical framework such as Coq, Isabelle
 or Abella, programming experience with a functional language such as 
OCaml, an understanding of proof theoretic treatments of aspects such as
 fixed-point definitions, and familiarity with issues related to 
proof search in sequent calculi and similar logical systems.<br><br>Please feel free to contact me (Gopalan Nadathur, <a href="mailto:ngopalan@umn.edu" target="_blank">ngopalan@umn.edu</a>)
 for more details about the position. To 
view the official announcement, please visit the URL<br><br>        <a href="https://hr.myu.umn.edu/jobs/ext/330828" target="_blank">https://hr.myu.umn.edu/jobs/ext/330828</a>.<br><br>This
 site also provides details about how to apply and serves as the portal 
for applications. A prerequisite for employment in this capacity is a
 doctoral degree in Computer Science or closely related field. <br></div><div class="gmail_default" style="font-size:small"><br></div><div class="gmail_default" style="font-size:small">-Gopalan<br></div></div></div>