Kim Nguyá»…n's Ph.D defense

Introduction

Kim Kim Nguyễn defended his Ph.D on the 7th May 2008, in Orsay. The title of the thesis is « Language of combinators for XML, conception, typing, implementation ».

Jury composition: V. Benzaken (Ph.D advisor), G. Castagna (Ph.D advisor), H. Hosoya, P. Thiemann, (reviewers), Ch. Paulin, Ph. Wadler

Abstract: We study in this thesis the design of a programming language for XML. Many existing works tackle this problem: main-stream languages coupled with XML libraries (C, Java, . . . ), “standardized” languages for XML (XSLT, XQuery, XPath), specialized languages (XDuce, CDuce, XTatic, . . . ) and lastly, restricted formalisms (k-peeble tree transducers, macro-tree transducers, regular expression filters). There are many flaws in these current approaches : main-stream and standardized languages do not take XML types into account (they are very lightly typed at best), specialized languages suffers from a complex type-system (requiring the programmer to heavily annotate his/her code), do not feature type inference and provide poor code modularity. Restricted formalisms, which seem to best fulfill our expectations are neither practical (macro-tree transducers, k-peeble tree transducers) nor sufficiently expressive (regular expression filters cannot encode XPath expression for instance). Our solution consists of a restricted language of combinators, dubbed filters, which features a precise typing policy, a type inference algorithm and are powerful enough to express complex XML transformations (XPath encoding, XSLT transformations, . . . ). The first part of this thesis is devoted to the theoretical definition of the core language, its semantics and its type system as well as a type inference algorithm. In a second part, we study practical aspects of this language such as its embedding in a full-fleged language (CDuce) and give an encoding of a non-trivial fragment of XPath into filters. We also show how to use the typing informations to optimize the loading of an XML document.

Résumé: Nous étudions dans cette thèse la conception d'un langage de programmation pour XML. De nombreuses approches à ce problème existent déjà : langages généralistes avec des bibliothèques XML (C, Java, …), langages « standards » pour XML (XSLT, XQuery, XPath), langages spécialisés (XDuce, CDuce, XTatic, …) et finalement, formalismes restreints (k-peeble tree transducers, macro-tree transducers, regular expression filters). Toutes ces approches souffrent de défauts : l'absence de discipline de typage « sérieuse » pour les langages généralistes et standards, un typage trop contraignant (nécessité pour le programmeur d'annoter lourdement le code, pas d'inférence de type, peu ou pas de modularité du code) pour les langages spécialisés. Les formalismes restreints, qui semblent répondre au problème sont soit difficilement utilisables en pratique (k-peeble tree transducers, macro-tree transducers) soit trop peu expressifs pour pouvoir exprimer des programmes intéressants (regular expression filters). Notre solution consiste en un langage restreint de combinateurs, appelés filtres, qui possède à la fois une discipline de typage précise, de l'inférence de type et une expressivité suffisante pour exprimer des transformations XML complexes (encodage d'XPath, transformations XSLT, …). Une première partie de la thèse est consacrée à la définition théorique du langage, sa sémantique, son système de type ainsi que la définition d'un algorithme d'inférence de types. Dans une seconde partie, nous étudions des aspects pratiques, tels que le plongement de ce langage restreint dans un langage plus généraliste (CDuce) et donnons aussi un encodage d'un fragment non trivial du standard XPath dans nos filtres. Nous montrons aussi comment utiliser les informations de typage pour optimiser le chargement d'un document en mémoire.

You can download the manuscript

See also: Cédric Miachon Ph.D defense.

Pictures

Some pictures taken by Sylvain Lebresne:

The very first slide Then after 45 minutes the last slide just before questions ... and all the jury members from left to right: Christine Paulin, Giuseppe Castagna, Véronique Benzaken, Phil Wadler and Peter Thiemann.