[TYPES] Post.Doc and Assist. Prof. position Radboud University
Nijmegen
Herman Geuvers
herman at cs.ru.nl
Mon Jul 4 17:43:14 EDT 2005
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
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.
More information about the Types-list
mailing list