Logic List Mailing Archive

3y postdoc position in computer science, Nijmegen (The Netherlands)

++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Radboud University Nijmegen - Institute for Computing and Information
Science

One 3 year post-doc position in the NWO-sponsored project

ARPA:    Advancing the Real use of Proof Assistants
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

We are seeking one researcher at the level of Postdoc for a period of 
three years, starting from September 1 2006

Candidates should have
-  Good knowledge of at least one and preferably more of the following
     fields: Hybrid Systems, Formal Methods, Proof Assistants and
             Automated Reasoning.
- A finished PhD in computer science, mathematics or logic


Description of the project
--------------------------
Proof Assistants help the user in developing a theory (stating
definitions and lemmas), modeling systems (describing constructions,
giving definitions) and verifying properties about these systems (giving 
proofs). So, Proof Assistants are very generic tools to support Formal 
Methods. Their genericity makes them less efficient than tools that are 
especially geared towards a specific formal method. On the other hand 
they have a very precise semantics, which makes a the certainty of a 
result that is verified by a Proof Assistant very high. This is 
especially the case for PAs that are able to produce "proof objects" 
that can be checked independently. In the future, the very high level of 
certainty will prevail. In this project we want to advance the use of 
PAs in several ways: (1) by developing a "mathematical input mode" for 
PAs, making theme more easy to use, (2) integration of different PAs, 
allowing the exchange of results, (3) developing a certified library for 
real number computation in Coq, (4) verifying hybrid systems in Coq, 
using the library of (3) to model and verify system properties. The 
quality of (3) will be judged by its applicability to (4), but (2) and 
(3) will also be judged by its applicability to the formalisation of the 
proof of Kepler's conjecture.

For detailed information see the full project proposal. It will be sent
to you on request (email to herman@cs.ru.nl).


The project leader is Dr. J.H. Geuvers. The research will be performed
within the research groups "Foundations" and "Informatics for Technical 
Applications" of the ICIS institute of the Radboud University Nijmegen, 
in collaboration with Prof.dr. F. Vaandrager (head of the ITA research 
group).

The research of the post-doc will be on topics (4) above.

Applications
------------
The full project proposal will be sent to you on request (herman@cs.ru.nl).
Further enquiries can be made with the project leader.

You are invited to send your application by email to the project leader.
Deadline for applications is June 25, 2006. In case you learn of this
job opportunity later than that date you may send an email to enquire
whether it still makes sense to apply.

Your application should consist of:

   - a curriculum vitae (containing information regarding your
     academic degrees, title of your PhD-thesis, publications)
   - the names and addresses of two referees