The Coq mailing list

[Femke van Raamsdonk <femke AT cs.vu.nl>]

=========================================================
Vrije Universiteit Amsterdam
PhD position in Theoretical Computer Science
Project title: Higher-Order Termination
=========================================================

A four year PhD position is available in the Section of 
Theoretical Computer Science of the Vrije Universiteit (VU)
in Amsterdam on the research project

  Higher-Order Termination (HOT)

The project
-----------
The goal of the project is to develop, extend, and improve 
methods to prove termination of higher-order rewriting systems.

Higher-order rewriting can be thought of as a combination 
of lambda calculus and first-order term rewriting. Termination
methods for higher-order rewriting need to deal with both
substitution, as in the lambda calculus, and algebraic 
manipulations, as in first-order term rewriting.

In the project we will study the higher-order recursive
path ordering and the dependency pairs method. We aim at
an integrated approach that is suitable both for rewriting
modulo alpha, and rewriting modulo alpha-beta-eta.
Further goals of the project are to study termination of 
type theory with rewriting (relevant for proof assistants),
and to contribute to the development of a higher-order 
termination tool.

For more detailed information on the project, please see

  http://www.cs.vu.nl/~femke/hot.pdf

The research will be carried out in the Section of Theoretical
Computer Science of the Vrije Universiteit. The main research
themes of the section are formal methods, term rewriting, 
lambda calculus, process algebra, coalgebra. The section has
various international cooperations.

Qualifications
--------------
Applicants should have a masters degree in computer science,
mathematics, logic, or a closely related area. Knowledge of
term rewriting and lambda calculus is considered an advantage.

Application
-----------
Please send applications by email to Femke van Raamsdonk
at 
femke AT cs.vu.nl.
 The deadline for application is August 1, 2007.
Your application should consist of a cover letter, a
curriculum vitae (including detailed information concerning
your academic degree, interests, and possibly publications),
and the contact details of two references.

Contact
-------
For further information about the project and the position
please contact

  dr. Femke van Raamsdonk
  
femke AT cs.vu.nl
  +31 (0)20 5987710