invited for a one-year postdoctoral
position at the University
. The position is available
immediately; applications will be reviewed as they are
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
for articulating properties of LF specifications, which has provided the basis for a proof assistant called Adelfa
for reasoning about such properties. In other work, we are developing
the capability to reason about linear logic specifications within the Abella proof assistant
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.
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
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
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
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.