[Agda] PhD student in the FormMath project

[Bas Spitters]

Job description
The aim of the FORMATH project(http://www.formath.cs.ru.nl) is to
develop libraries of formalized mathematics concerning algebra, linear
algebra, real number computation, and algebraic topology:
These libraries will be structured as software components, relying on
Ssreflect, which has proved its worth in the formal proof of the four
colour theorem, and to address topics that were mostly left untouched
by previous research in formal proofs or formal methods.

This work concerns formally proved algorithms for solving problems in
real arithmetics, solving problems in ordinary differential equations,
or solving problems in algebraic topology.
Our methodology is a combination of theoretical research and
technological development. The main tools will be provided by the
Mathematical Components project, for instance the Ssreflect library
for Coq proof assistants.

The four partners in the EU ForMath project are:
- Goteborg;
- INRIA;
- Nijmegen;
- La Roja.

More specifically, as a PhD student at the Nijmegen location you will
work on Work package 4;
- Real number computation and basic numerical analysis;
- The use of exact real number computation to prove inequalities.

The objective is specification and implementation of a simple ODE
solver. Potential fields of applications include robotics and hybrid
systems.

Requirements
You should meet the following requirements:
- A master's degree (or equivalent) in Computer Science, Mathematics
or a related field, with a strong interest in proof assistants, type
theory, functional programming, constructive analysis and numerical
analysis;
- Commitment and a cooperative attitude;
- Excellent proficiency in written and spoken English.

Organization
The Radboud University Nijmegen is one of the leading academic
communities in the Netherlands. Renowned for its green campus, modern
buildings, and state-of-the-art equipment, it has nine faculties and
enrols over 17.500 students in approximately 90 study programmes. The
university is situated in the oldest Dutch city, close to the German
border, on the banks of the river Waal (a branch of the Rhine). The
city has a rich history and one of the liveliest city centres in the
Netherlands.
The section Intelligent Systems of the Institute for Computing and
Information Sciences (ICIS) at the Radboud University Nijmegen studies
mathematical theories concerned with computability, provability and
complexity. Notably, the group studies type theory, lambda calculus
and logic and also applies these theories in the area of theorem
proving and formalizing mathematics.
The group has an excellent international reputation which was
supported by the last national research assessment.
Website: http://www.cs.ru.nl

Conditions of employment
Employment: 1,0 fte
Maximum salary per month, based on a fulltime employment: € 2,612 gross/month
Starting at € 2,042 per month, the salary will increase to € 2,612 per
month in the fourth year.
PhD scale.

Additional conditions of employment
You will be appointed as a PhD student for a period of four years.
Your performance will be evaluated after 18 months. If the evaluation
is positive, the contract will be extended by 2.5 years.

Additional Information
Bas Spitters
Telephone: +31 24 3652611
E-mail: spitters at cs.ru.nl
Telephone: +31 24 3652104

Application
You can apply for the job (mention the vacancy number 62.52.09) before
1 February 2010 by sending your application -preferably by email- to:

RU Nijmegen, FNWI, P&O, mrs. D. Reinders
P.O. Box 9010, 6500 GL Nijmegen, NL
Telephone: +31 24 3652027
E-mail: pz at science.ru.nl
http://www.ru.nl/vacaturedetails?recid=497982