[TYPES/announce] PhD position at ENS Cachan on query languages with data: proof systems and complexity

[David Baelde]

Please forward this announcement to potentially interested students.


--------------------------- Phd Position ----------------------------

                    Query Languages with Data:
                   Proof Systems and Complexity

                     LSV, ENS Cachan, France

---------------------------------------------------------------------


One PhD position, fully funded, is open at LSV, ENS Cachan, to start
in the Autumn, 2015.

The applicant should have a strong background in theoretical computer
science, including expertise is at least two of the following domains:

 - logic, in particular modal logic;
 - proof theory;
 - complexity theory.

The PhD is funded for three years, with a gross salary of €1,757 per
month, which amounts to about €1,400 after tax.  The position also
comes with opportunities to teach after the first year (at ENS Cachan
or elsewhere in the Parisian area), which yield extra salary
(it then typically reaches about €1,800 after tax).

The LSV is a small but thriving lab with a leading expertise in formal
verification.  It has a lively atmosphere, with regular seminars and
an `open doors' policy, and an international staff.  It is very well
located, with the Parisian area being one of the international hot
spots of logic and theoretical computer science.

To apply, send a CV (including passed courses and grades), a
motivation letter as well as references, before September 5th, by
email to:

 - David Baelde <baelde at lsv.ens-cachan.fr>
 - Sylvain Schmitz <schmitz at lsv.ens-cachan.fr>

Please do not hesitate to contact us if you have any question,
prior to a formal application.


-- Background

The PhD is founded by the ANR project Prodaq, whose scientific
objectives are described in broad terms below.  The PhD topic will
include several of the research axes of the project, depending on the
student's inclinations.

Semi-structured data, in particular in the form of XML documents, is
now an established paradigm for storing and retrieving data over the
Internet.  XPath is a querying language, which allows to select
elements in XML documents.  Its use is pervasive in Web-oriented
languages like XSLT or XQuery, but also in general-purpose languages
like Java or C#.  A data-aware, fully automated formal analysis of
XPath is however in general impossible due to undecidability results.

The research on restrictions and variants of XPath therefore seeks new
standards, algorithms, and languages, which should strike a balance
between practical usability---can typical queries be expressed in the
restricted language?---and amenability to formal analysis---can we
check queries written in the language?

In this context, the main objective of the project is to investigate
the proof theory of data logics like XPath.  Proof systems will be
used both as theoretical tools (to derive complexity results and to
investigate the relationships with other logics), and as practical
tools (by implementing proof search procedures).