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.