[Agda] 1yr researcher on the formath project

[Bas Spitters]

We seek a researcher (either on the postdoc or gradaute student level)
to work on the formath project for 1yr.
The research will be carried out at Radboud University Nijmegen (NL).

Extensive experience with Coq or similar provers is desirable.

www.tinyurl.com/formath

AIMS OF THE PROJECT
===================
The aim of the FORMATH project is to develop libraries of formalized
mathematics concerning algebra, linear algebra, real number
computation, and algebraic topology. The main originality of this work
will be to structure these libraries as a software development,
relying on a basis of ssreflect that has already shown its power in
the formal proof of the four color theorem, and to address topics that
were mostly left untouched by previous research in formal proof or
formal methods.
The main milestones of this work will concern formally proved
algorithms for solving problems in real arithmetic, solving problems
in ordinary differential equations, or solving problems in algebraic
topology.

The ForMath EU-project consists of four partners:
- Goteborg
- INRIA
- Nijmegen
- La Roja

Specifically, you will work on
Computation with Real Numbers (WP4)
Challenges:
- Develop formally verified numerical analysis.
- Provide the basis for numerical computations inside formal proofs.
- Develop a high level programming language for numerical analysis.
-----------------------------------------------------------------
Application:
Deadline for application is December 1st, 2011.
Send an application letter with CV and a reference to Bas Spitters
(spitters at cs.ru.nl).