The Coq mailing list

[Herman Geuvers <herman AT cs.ru.nl>]

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

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

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

We are seeking one researcher at the level of Postdoc and one Assistant
Professor (UD) for a period of three years, starting from September 1 2005

Candidates should have
-  Good knowledge of at least one and preferably more of the following
   fields: Type Theory, Proof Assistants, Formalizing Mathematics,
           Logic and Automated Reasoning.
 - For a postdoc position: a finished PhD in computer science,
   mathematics or logic
 - For an Associate Professor (UD) position: additional experience in
   education.


Description of the project
--------------------------
Proof Assistants help the user in developing a theory (stating 
definitions and lemmas), model ling 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 positions
-------------
The project leader is Dr. J.H. Geuvers. The research will be performed 
within the research group "Foundations" of the ICIS institute of the 
Radboud University Nijmegen, in collaboration with Prof.dr. H.P. 
Barendregt and partly in collaboration with Prof.dr. F. Vaandrager from 
the "Informatics for Technical Applications" research group.

The research of the post-doc will be on topics (1) and (2) above. The 
Assistant Professor will have a 50% research - 50% education task; the 
research of the Assistant Professor will be on topic (3) above.
(Research on topic (4) will only start in September 2006, when a second 
post doc research position will become available.)


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 July 14, 2005. 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

Please indicate clearly in which of the two positions you are interested.