Email Gateway (Aug 22 2022 at 19:57): Email Gateway (Aug 22 2022 at 19:57):From: Gopalan Nadathur <gopalan@cs.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@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.
Email Gateway (Aug 22 2022 at 20:36):From: Gopalan Nadathur <gopalan@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 outlined 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 are 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@umn.edu.
-Gopalan Nadathur
Last updated: Apr 26 2024 at 08:19 UTC