The Coq mailing list

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

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