[TYPES/announce] Postdoctoral Opening at the University of Minnesota

[Gopalan Nadathur]

Applications are invited for a one-year postdoctoral position at the
University of Minnesota. The position is available immediately;
applications will be reviewed as they are received.

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
new logic <https://arxiv.org/abs/2107.00111> for articulating properties of
LF specifications, which has provided the basis for a proof assistant
called Adelfa <http://adelfa.cs.umn.edu> for reasoning about such
properties. In other work, we are developing the capability to reason about
linear logic specifications within the Abella proof assistant
<https://abella-prover.org/> 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.

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.

Please feel free to contact me (Gopalan Nadathur, ngopalan at umn.edu) for
more details about the position. To view the official announcement, please
visit the URL

        https://hr.myu.umn.edu/jobs/ext/330828.

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.

-Gopalan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20210730/9f30debb/attachment-0001.htm>