1 POSTDOC and 1 PHD POSITION in the MathWiki project
at Radboud University Nijmegen (NL)
The Institute for Computing and Information Science of the Radboud University Nijmegen (NL) is looking for 2 researchers to work on the NWO project "MathWiki a Web-based Collaborative Authoring Environment for Formal Proofs".
The vacancies are:
a Post-doc position for the period of 3 years, vacancy number: 62-16-09
a PHD POSITION for the period of 4 years, vacancy number: 62-17-09
Aims of the project
The aim of the MathWiki project is to open up to a wider community the rich collections of knowledge stored in the repositories of proof assistants.
To this end we will build a web-based collaborative authoring environment for formal mathematics, the MathWiki system. This system will provide interactive web access through a standardized interface to a number of proof assistants. The MathWiki system will also be a platform for the development of formal proofs within those proof assistants and it will provide high level access (through Wikipedia-like web pages) to their repositories of formalised mathematics. These repositories will reside on the server.
In the project we will study and further develop Wiki technology and semantic web technology, all in the context of proof assistant repositories of formalized mathematics. The project thus brings together the open nature of Wiki authoring with expertise in Proof Assistants and Semantic Web technologies to build a new Wiki for mathematics, supporting content creation, search and retrieval.
From the perspective of the ordinary user of mathematics, MathWiki will be important because it will provide high-level mathematical content on the web in a much more coherent and precise way than is available at present.
From the proof assistant user perspective, MathWiki will be important because it will provide an advanced environment for the collaborative authoring of verified mathematics, mediated simply by a web interface.
The MathWiki system will be based on our existing experience with proof assistant technology on the web, the "ProofWeb" systems, see http://prover.cs.ru.nl
The concrete goals of the project are to:
Provide a web-based generic authoring environment for proof assistants.
Build a Wiki platform for the disclosure of repositories of formal proofs.
Provide methods and tools for high level generic search of mathematical notions.
Develop techniques for high level step-wise refinement of mathematical (formal) proofs.
Requirements for the PhD student position
A master's (or equivalent) degree in Computer Science, Mathematics or a related field, with a strong interest in proof assistants and/or semantic web technology (preferably both)
Commitment and a cooperative attitude.
Very good written and oral English skills.
The junior researcher is intended to work on
Searching facilities for mathematics, notably semantically rich search through the repositories of formalized mathematics. Every proof assistant has its own ad-hoc search engine, usually only able to search inside the part of the library that has been previously explicitly loaded by the user. In the proof assistant community, there are no general solutions for indexing and searching, that can be uniformly applied to all formal libraries. We will use the OMDoc standard and experience gained in the Whelp project (Univ. of Bologna) to build semantically rich search functionality, integrating existing search functions in proof assistants.
The development of a high level proof language, using which one can formalize proofs via a step-wise refinement method. So, we will develop a work-flow for evolving unstructured natural language text step by step into a formal representation. In our research team we have developed some ideas on how to do that, via the notion of “Formal Proof Sketches” and an we have developed an initial implementation of a declarative proof language in Coq.
Requirements for the Postdoc position
A PhD in Computer Science, Mathematics, or a related field with expertise in proof assistants and/or semantic web technology (preferably both).
A strong publication record.
Commitment and a cooperative attitude.
Very good written and oral English skills.
The post-doc is intended to work on
The interaction model for proof assistants. We have experience in developing a web-interface for the proof assistant Coq that has been adapted -- in prototype -- to Isabelle. The post-doc should cooperate with the developers of proof assistants and possibly with the developers of Proof General, the generic emacs interface for proof assistants that is one of the standard interfaces for both Coq and Isabelle.
The Wiki base for the MathWiki web-pages. This will be based on experience in developing a first MathWiki prototype. We will build this Wiki on existing experience with semantic Wiki's, like IkeWiki and SWiM and for our encoding we will use XML-standards like OpenMath and OMDoc to make optimal use of existing semantic web technology for (formal) mathematics.
The functionality to make cross-links between various entries of different repositories. This way, one can easily link a lemma in one system to a lemma in another, or an unproven result in one system to a lemma in another, thereby “reusing” the proven result.
Conditions of employment
The PhD students will be employed for a period of 4 years (40 hrs/week). The Postdocs will be employed for a period of 3 years (40 hrs/week). Supervision for the projects will be done by Prof. Dr. Herman Geuvers and Dr. F. Wiedijk
Postdoc and PhD student will be appointed by the Radboud University Nijmegen. Both positions shall start before October 1 2009, but preferably earlier.
The salary for the PhD position starts at 2042 Euro per month, increasing to 2612 Euro per month in the fourth year.
The maximum salary for the Postdoc is 3755 Euro per month (salary scale 10).
Information
For inquiries about the project and its positions, please contact the project leader Prof. Dr. Herman Geuvers ( H.Geuvers@cs.ru.nl , +31 243652603). Interested candidates can ask the project leader for the complete project application text.
Application
Deadline for application is May 1, 2009.
Send an application letter with CV and 3 references, mentioning the vacancy number by e-mail to
RU Nijmegen, FNWI, P&O mrs. D. Reinders Postbus 9010 6500 GL Nijmegen Netherlands
e-mail: pz@science.ru.nl telephone: +31 243652764