[TYPES] research vacancies in Amsterdam (VU, CWI) and Utrecht

[Roel de Vrijer]

=======================================================================
Vrije Universiteit Amsterdam  ++  CWI Amsterdam  ++  Utrecht University

Three research positions in the NWO-sponsored project
   INFINITY:    Infinite Objects, computation, modeling and reasoning
=======================================================================

We are seeking three researchers at the level of Postdoc or Asssociate
Professor (UD) for a period of two to three years.

Candidates should have

-  Good knowledge of at least one and preferably more of the following
   fields: Term rewriting, Graph rewriting, Lambda calculus, Proof theory,
   Co-algebra, Co-induction, Logic and Automated Reasoning, Type theory
 - For a postdoc position: a (nearly) finished PhD in computer science,
   mathematics or logic
 - For a UD position: several additional years of research experience

Starting date of the project is September 1st, 2005.


Description of the project
--------------------------

We consider infinite objects, such as streams, infinite trees, infinite
terms and term graphs, both first order and higher order (with binders as
in lambda calculus) or infinite communicating processes. Often these
exhibit a regular or cyclic nature, but we are also interested in general
infinite objects. A paradigm example is the coalgebra of infinite
bitstreams. Several operators can be defined on these objects, such as the
operator zip that zips two streams alternatingly into one. Defining

   ones = 1 : one          zeros = 0 : zeros        alt = 0 : 1 : alt

we have equations such as


   zip(zeros, ones) = alt

The equations holding in this coalgebra between these objects and their
operators can be proved in three different ways: by coalgebraic
techniques, by proof theory, and by infinitary term rewriting. These three
methods have been developed up to now in relative isolation. This project
investigates the relations between these approaches and aims to design
methods such as new proof systems to deal with the infinite objects and
their equations. Issues are well-definedness criteria, completeness of the
methods, decidability and implementation. Thus the project combines for
infinite objects the activities of computing, modeling, and reasoning.

For detailed information see the full project proposal. It will be sent
to you on request (email to rdv at cs.vu.nl, please mention "INFINITY" in
the subject).


The positions
-------------

The project is headed by Prof. Dr. J.W. Klop and is a collaboration
between the following Dutch research groups:

 - Vrije Universiteit Amsterdam, section "Theoretical Computer Science"
   contact:  Dr. R.C. de Vrijer,  rdv at cs.vu.nl, phone: +31 (0)20 5987770

 - CWI Amsterdam, the group "Coordination languages"
   contact:  Prof. Dr. J.J.M.M. Rutten, jan.rutten at cwi.nl

 - Utrecht University, the group "Theoretical Philosophy"
   contact:  Dr. V. van Oostrom, Vincent.vanOostrom at phil.uu.nl

The research will be embedded in the broader framework of the themes of
the three participating research groups: formal methods, logic, term and
graph rewriting, lambda calculus, coalgebraic methods, process algebra.

At each institution there is one position available. Roughly the focus
of the three positions varies as follows, more details to be found in
the full proposal.

 - Vrije Universiteit: Proof theory, Infinitary term rewriting
 - CWI: Co-algebra, theory and applications
 - Utrecht University: Infinitary term rewriting and implementation
   using graph rewriting


Applications
------------

The full project proposal will be sent to you on request (rdv at cs.vu.nl).
Further enquiries can be made with the contact persons.

You are invited to send your application by email to the contact person of
the institution for which you want to apply. Deadline for applications is
July 17, 2005. In case you learn of this job opportunity later than that
date you may send an email to enquire whether it still makes sense to
apply.

Your application should consist of:

 - a cover letter
 - a curriculum vitae (including detailed information regarding your
   academic degrees, title and subject of your PhD-thesis, publications)
 - the names and addresses of two references

If you are interested in more than one of the offered positions you should
clearly indicate so and give your motivation. It is not necessary to write
separate letters.

Please include "INFINITY" in the subject of all your emails.