[TYPES/announce] Post Doc position Radboud University Nijmegen

[Herman Geuvers]

++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
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), modelling 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 at 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 at 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