[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 related to an NSF-funded project entitled "A
Higher-Order Framework for Meta-Theoretic Reasoning." The position is
available immediately and reviews of applications will be conducted 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. A defining characteristic of the
project is its focus on the so-called higher-order abstract syntax approach
to representing objects that embody a binding structure. Ongoing work is
aimed at developing systems for reasoning about specifications encoded in
linear logic as well as in the dependently typed lambda calculus LF. The
group is also interested in furthering its earlier work that has
demonstrated the benefits of higher-order representations of syntax in the
verification of compilers and transformers for functional programming
languages. Another direction of investigation is that of enhancing the
logic underlying the  Abella proof assistant (see http://abella-prover.org)
with the capability of predicate quantification and on exhibiting the
usefulness of such an enhancement through a collection of targeted
reasoning applications. 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 help 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 induction and co-induction,
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 topics of research within the project, the necessary
background and other relevant 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. The application process will require you to submit a
letter indicating your interest, a current CV, one or two of your papers
broadly related to the topics of research and the names and contact details
for two references who might be contacted as part of the application review
process. Note that a prerequisite for employment is a doctoral degree in
Computer Science or closely related field.

-Gopalan Nadathur
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20200603/b8fae29f/attachment.html>