Vacancy for Ph.D. student (Netherlands)

In the Faculty of Mathematics and Computer Science,
Technical University Eindhoven, The NETHERLANDS,
there is a job opportunity for a Ph.D. student.

The student will be placed in the Formal Methods group of the
Department of Computer Science, headed by Prof. Jos Baeten.
The Formal Methods group (http://www.win.tue.nl/cs/fm/)
works on various topics, including Proces Algebra, Verification and
Specification and Type Theory and Theorem Proving. 

The Ph.D. student will work on the project (sponsored by NWO, the
Dutch organisation for fundamental research) titled

"Use and Meaning of Open Terms in Interactive Formal Problem Solving"

under supervision of Dr. R. Nederpelt and Dr. H. Geuvers.
See the abstract of the project proposal below.

In the Netherlands, A Ph.D. student is a member of the faculty
staff and has a position for four years. The income is Dfl 2843,-
in the first year, increasing to Dfl 3841,- in the fourth year.

We are looking for someone who holds a Master's in Mathematics or
Computer Science with a background in either logic or formal methods.

For more information (including a full project proposal), look at
or  contact
Dr. R. Nederpelt, e-mail wsinrpn@win.tue.nl, tel. 31 (0)40 2472718
Dr. H. Geuvers, e-mail herman@win.tue.nl, tel. 31 (0)40 2472999 

By formal problem solving, we mean problem solving where the problem
and the possible solutions are stated in a precise way, and so is the
notion of correctness, stating whether a solution solves a
problem. Formal problem solving occurs in many places in computer
science, like a program editor (where a program has to meet a
specification), a structure editor (where syntactically correct
expressions have to be built), verification (of protocols), testing,
theorem proving and data bases (where information is extracted using
queries). An important aspect of computer systems for problem solving
is that they are interactive. The machine will in general not be able
to solve our problems by itself; solving problems requires
human-machine interaction. Ideally, one would let the computer
construct a part of the solution, returning a `solution-with-holes',
and then the user provides information on how to proceed to refine the
holes. Such a hole in a `solution-with-holes' is also known as an open
term: a term containing (a special kind of) variables, for which
instantiations have to be found. In general, the formal meaning of
these open terms is not very clear, but they work for the purpose of
the human-machine interaction. We will investigate these open terms
both from the perspective of usability, as from their meaning in the
underlying formal theory. The starting point will be type theory
with open terms, which are implemented as interactive theorem provers.