[TYPES/announce] Postdoc position on Typefull XML at LRI Univ. Paris-Sud

[Kim Nguyen]

      Postdoctoral position on Typeful and Certified XML
       Université Paris Sud - INRIA - Saclay available.

     [Planned start date: fall 2012 - early winter 2013]

********************************************************************


Applications are invited for a postdoctoral position at LRI -
Université of Paris Sud 11, ProVal - Proof of programs group joint
group with INRIA Saclay Île de France.

http://proval.lri.fr/

The selected candidate will have to conduct research in the area of
programming languages, data-centric programming languages, and
XML. The research will take place in the context of the ANR project
Typex: Typeful and Certified XML:

http://typex.lri.fr/index.html


Profile:
--------

Candidates must have a PhD in Computer Science with a strong
background in type theory, functional programming and programming
language design.  Skills in an additional area of computer science
(proof theory, interactive theorem provers, etc.) are very welcome.
The term of the postdoc position is one year and half (18
months). Starting date is negotiable (tentatively September 2012).
The expected salary is about 2400 euros net income (4400 gross income)
per month depending on the experience of the candidate.

Application:
------------

To apply, send a resume, a brief statement of interest, and names of
at least two references to:

Veronique Benzaken (veronique.benzaken at lri.fr) and
Kim Nguyen (kn at lri.fr)


Detailed research plan: Toward a typeful XQuery
-----------------------------------------------

XQuery [1], the W3C XML query language, blends in its upcoming 3rd
version usual declarative constructs (FOR loop, akin to list
comprehension, ORDER BY, XPath [2] queries, ...) and functional traits
(higher order, pattern-matching, ...).

In parallel, recent progress has been made [3,4] on the front of
functional languages for XML. In particular the CDuce language
features full regular expression types, a powerful pattern-matching
construct, a powerful subtyping relation and type algebra (allowing
amongst other things, higher-order functions, overloading, extensible
records, ...). A missing feature (namely parametric polymorphism) has
recently been added [5].

Topic of research:
-----------------------

The goal of this postdoc position is to bridge the gap between XQuery
and CDuce by porting the advanced typing features of CDuce to XQuery.
A first work is to define a functional core of XQuery 3 (similar to
the XQuery Core [6] but taking into account higher order). While close
this Core XQuery would remain different from CDuce in one key aspect:
use of path expression instead of pattern-matching as querying
primitives.

With this core language in place, a second goal is to adapt the rich
type system of CDuce to XQuery 3 Core, in particular by adding some
polymorphic traits to XQuery's existing type system (by extending it if
necessary)

[1] http://www.w3.org/TR/xquery-30/

[2] http://www.w3.org/TR/xpath/

[3] http://www.cduce.org

[4] A. Frisch, G. Castagna, and V. Benzaken: Semantic Subtyping:
dealing set-theoretically with function, union, intersection, and
negation types. Journal of the ACM, vol. 55, n. 4, pag. 1―64, 2008.

[5] G. Castagna and Z. Xu: Set-theoretic Foundation of Parametric
Polymorphism and Subtyping. In ICFP '11: 16th ACM-SIGPLAN
International Conference on Functional Programming, pag. 94-106,
September, 2011.

[6] http://www.w3.org/TR/xquery-semantics/

-- 
Kim