[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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: spitt...@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: p...@science.ru.nl http://www.ru.nl/vacaturedetails?recid=497982