The Coq mailing list

[Gopalan Nadathur <gopalan AT cs.umn.edu>]

Postdoctoral Opportunity at the University of Minnesota

Applications are invited for a 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 is expected to be of duration of one to two years. Applications will be reviewed and acted upon as soon as they are received.

The project within which the appointment is to be made concerns the further development of a proof environment for reasoning about relational specifications that supports the so-called higher-order abstract syntax approach. A key component of this environment is the Abella proof assistant (see http://abella-prover.org), which is based on a logic that incorporates a treatment of fixed-point definitions. One thrust for ongoing work is the enhancement of the underlying logic, for example through the addition of predicate quantification. The research group is also interested in building into the Abella system the capability to reason about specifications written in linear logic and dependently typed lambda calculi, and in investigating the benefits of the system in tasks such as compiler verification.

To participate successfully in the research described above, you would need to be broadly conversant with the areas of computational logic and programming languages and to have the mathematical and programming skills necessary for conducting original work in these areas. 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 other similar logical systems would help in engaging immediately with the research problems of interest.

To view the official announcement for this position, please visit the URL
      https://hr.myu.umn.edu/jobs/ext/330828.
This site also provides details such as the required qualifications for the position and serves as the portal for applications. To complete an application, you would need to submit a letter indicating your interest in the position, a current CV, one or two papers broadly related to the topics of research and the names and contact details of two people who are willing to serve as your references in the review process.

Please do not hesitate to contact me if you have an interested in the position but would like answers prior to applying to questions related to matters such as the expectations, possible projects, and the suitability of your qualifications for the position. The best way to reach me would be via email sent to ngopalan AT umn.edu.

-Gopalan Nadathur