Email Gateway (Aug 19 2022 at 08:20): Email Gateway (Aug 19 2022 at 08:20):From: Gopalan Nadathur <gopalan@cs.umn.edu>
Applications are invited for a one-year postdoctoral position at the
University of Minnesota related to an NSF-funded project entitled
"Reasoning about Specifications of Computations." The position is
available immediately: to guarantee consideration, applications must
be received before September 7, 2012.
The project within which the appointment is to be made concerns the
areas of computational logic and programming languages. To be suitable
for the position, the candidate should be broadly conversant with the
issues in these areas and should have the mathematical and programming
skills necessary for conducting research in them. Moreover, with
suitable mentoring, he/she should be capable of developing an
independent research agenda that encompasses some of the following
topics:
the design of logics for specifying computational systems and
for reasoning about such specifications,
the implementation of systems embodying such logics, and
the use of the implemented systems in constructing actual
specifications and reasoning about them.
Facility with proof assistants and logical frameworks such as Coq,
Isabelle and Twelf, 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 related logical systems
would be needed for participating in the research at the appropriate
level. A specific focus for the project is the Abella system (see
http://abella.cs.umn.edu), developed originally at the University of
Minnesota and currently also the subject of work within the Parsifal
project at Ecole Polytechnique and INRIA, Saclay. The ideal candidate
would have an interest in further developing the capabilities of this
system and its applications during the appointment period.
To apply for this position, go to the U of M Employment System at
https://employment.umn.edu/ and search postings with req#: 179943. The
online application process will require you to submit a current CV and
a brief research statement that should describe past research and
future plans in a way that addresses appropriateness for the position
advertised. Please also provide names, phone numbers and email
addresses of two or three references as part of this material; these
references may 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.
Interested individuals are encouraged to contact Gopalan Nadathur at
gopalan@cs.umn.edu for more information towards assessing the
suitability of an application.
Email Gateway (Aug 23 2022 at 09:17):From: Gopalan Nadathur <gopalan@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@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
Last updated: Nov 21 2024 at 12:39 UTC