ℂDuce: Contacts: Pictures and Logos: Zhiwu Xu's Ph.D defense

## PhD defense

Zhiwu Xu defended his PhD thesis on the 30th of May 2013, in Beijing. The title of the thesis is Â« PARAMETRIC POLYMORPHISM FOR XML PROCESSING LANGUAGES Â».

**Jury composition:**
Frederic BLANQUI,
Giuseppe CASTAGNA (advisor),
Haiming CHEN (co-advisor),
Mariangiola DEZANI (reviewer),
Xinyu FENG (reviewer),
Giorgio GHELLI (reviewer),
Huiming LIN

**Abstract:**
XML (eXtensible Markup Language) is a current standard format for exchanging semi-structured
data, which has been applied to web services, database, research on formal
methods, and so on. For a better processing of XML, recently there emerge many statically
typed functional languages, such as XDuce, CDuce, XJ, XTatic, XACT, XHaskell,
OCamlDuce and so on. But most of these languages lack parametric polymorphism
or present it in a limited form. While parametric polymorphism is needed by XML
processing, this is witnessed by the fact that it has repeatedly been requested to and
discussed in various working groups of standards (e.g., RELAX NG and XQuery).
We study in this thesis the techniques to extend parametric polymorphism into XML
processing languages.
Our solution consists of two parts: a definition of a polymorphic semantic subtyping
relation and a definition of a polymorphic calculus. In the first part, we define and
study a polymorphic semantic subtyping relation for a type system with recursive,
product and arrow types and set-theoretic type connectives (i.e., intersection, union and
negation). We introduce the notion of â€œconvexityâ€ on which our solution is built up and
prove there exists at least one model that satisfies convexity. We also propose a sound,
complete and terminating subtyping algorithm. The second part is devoted to the
theoretical definition of a polymorphic calculus, which takes advance of the subtyping
relation. The novelty of the polymorphic calculus is to decorate Î»-abstractions with
sets of type-substitutions and to lazily propagate type-substitutions at the moment of
the reduction. The second part also explores a semi-decidable local inference algorithm
to infer the set of type-substitutions as well as the compilation of the polymorphic
calculus into a variety of CDuce.

You can download the manuscript from the TEL server.

ℂDuce: Contacts: Pictures and Logos: Zhiwu Xu's Ph.D defense