[TYPES] PhD vacancy at the VU

[Roel de Vrijer]

===================================================
Vrije Universiteit Amsterdam
PhD position in Theoretical Computer Science
Project title: Proving equations for cyclic objects
===================================================

In the Section of Theoretical Computer Science of the Vrije Universiteit 
in Amsterdam there is a position for a PhD student for 4 years on the 
research project

           Proving Equations For Cyclic Objects

Starting date of this PhD position is as soon as possible.

The project
----------- 

This project considers equations between infinite objects, such as streams
of 0 and 1. An example equation is 

       morse = 1:0:zip(tail(morse),inv(tail(morse))) 

defining the famous Thue-Morse sequence 1001011001101001..., satisfying 
the equation odd(morse) = morse. While proof systems for infinite regular 
objects are well-known, we study in this project proof systems for more 
general infinite objects, also non-regular, such as the example stream. We 
aim to develop and study proof systems of various nature, employing 
fixed-point rules, coinductive proof rules, or proof procedures based on 
bisimulation. Relations with coalgebra will be explored as well as with 
infinitary term rewriting. Aspects of definability of infinite objects will
be investigated. Where possible, theory will be developed that is relevant 
for automated equation provers.

For more detailed information see the full project proposal at:

  http://www.cs.vu.nl/~tcs/ProvCyc.pdf

The research will be in the broader framework of the section's main 
themes: formal methods, term rewriting, process algebra, coalgebra.


Qualifications
-------------- 

Candidates must have a masters degree in computer science, mathematics or 
logic, preferably with knowledge of topics such as automata theory, lambda 
calculus, type theory, term rewriting or proof theory.


Contact and application
-----------------------

For further information about this position please contact:

  Prof.dr. J.W. Klop,  jwk at cs.vu.nl, phone: +31 (0)20 5987770 or
  Dr. R.C. de Vrijer,  rdv at cs.vu.nl, phone: +31 (0)20 5987770

You are invited to send an application by email to rdv at cs.vu.nl, no later 
than May 1, 2005. Your application should consist of a cover letter, a 
curriculum vitae (including detailed information regarding your academic 
degree and possible publications) and the names and addresses of two 
references.