The Coq mailing list

[Gopalan Nadathur <ngopalan AT umn.edu>]

Postdoctoral Opportunity at the University of Minnesota

Applications are invited for a one-year postdoctoral position, possibly extendable into a second year, 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 further development of a logic that incorporates a treatment of fixed-point definitions and the enhancement of the capabilities of the Abella proof assistant (see http:\\abella-prover.org) that is based on this logic. One particular extension to the underlying logic that is being investigated is 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 demonstrating the benefits of the system in tasks such as compiler verification.

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. 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 be needed for participating in the research at the appropriate  level. For more details about the necessary background and possible topics of research within the project, please feel free to contact me (Gopalan Nadathur) via email at ngopalan AT umn.edu.

To view the official announcement for this position, please visit the URL
      https://hr.myu.umn.edu/jobs/ext/330828.
This link 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.