[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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 ngopa...@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.