[isabelle] Postdoctoral Opening at the University of Minnesota

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 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.

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 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


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 Nadathur

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.