[Agda] Post-doctoral position in interactive theorem proving at the University of Iowa

[Chantal Keller]

-----------------------------------------------------
Post-doctoral position in interactive theorem proving
Computational Logic Center
Department of Computer Science
The University of Iowa
-----------------------------------------------------

Applications are invited for a post-doctoral research position in the 
Computational Logic Center at the University of Iowa in the area of 
interactive theorem proving and verification.

The position is funded by DARPA through the HACMS program. The work will 
be done in collaboration with researchers at New York University, the 
Université Paris Sud and Princeton University. The main goal of the 
project is to increase the level of automation in the Coq proof 
assistant by soundly integrating SMT solvers into it. Our immediate 
emphasis is on supporting software verification efforts by other 
research groups currently funded by HAMCS. However, we expect that the 
results of the integration will benefit Coq users in general.

The ideal candidate will have a Ph.D. in Computer Science, general 
knowledge of formal methods, and expertise in interactive theorem 
proving in higher-order logics, with substantial experience in using 
Coq, Isabelle, or similar tools. Candidates should demonstrate strong 
programming and formal modeling skills. Previous experience in writing 
Coq tactics and plug-ins is a considerable plus. Familiarity with SMT is 
welcome but not required.

The position is a full time appointment that runs initially through 
August 2016 and could be renewed for another year subject to 
satisfactory performance and continuous availability of funds. Review of 
applications will begin immediately. The position will remain open until 
filled. The start date is negotiable, but ideally it should be as soon 
as possible. The starting salary is $56,000 per year, plus health and 
vacation benefits.

Depending on the candidate's interests, there might be also be a 
possibility to teach one course in the spring semester in the Computer 
Science department as a visiting assistant professor. This is, however, 
a separate position that would entail a corresponding reduction of 
effort for the postdoc appointment. It should be understood as an 
opportunity, not as a requirement for the postdoc contract.

Inquiries and applications should be sent via email to 
cesare-tinelli at uiowa.edu with "Coq postdoc" in the subject. When sending 
an application please include your CV together with a brief description 
of your research accomplishments and interests, including the names of 
three references.


---
The Computational Logic Center at the University of Iowa is jointly 
headed by Professors Aaron Stump and Cesare Tinelli. In recent years, it 
has consisted on average of two faculty members, 3-5 postdocs, 6-7 PhD 
students and a few master's and undergraduate students. Its work has 
been funded by the AFRL, AFOSR, DARPA, NASA, NSF, Intel, Rockwell 
Collins, and United Technologies.
Its main areas of research are automated deduction, satisfiability 
modulo theories, software verification, model checking, 
verified-programming languages, and foundations of programming 
languages. The center has a strong emphasis on theoretical foundations 
but is also known for a number of languages and tools co-developed with 
external partners and used in academia and industry. These include the 
SMT-LIB standard, the CVC3 and CVC4 SMT solvers, the Kind and Kind 2 
model checkers, the LFSC proof framework and checker, the Darwin theorem 
prover, and the StarExec solver execution service.