+1 Thank you, Hello, Joint work with …
+
+2 XQuery (3.0) looks like that: 2 functions …
+ Path expressions to navigate
+ List comprehension syntax
+ type-switch case
+ switch case
+
+3 Pros and Cons of XQuery
+
+4 CDuce : Syntax similar to OCaml
+ Patterns (in part. XML constructs with tag, attributs, list of children)
+ Types! (with constructors, intersections, …)
+ List comprehension too.
+
+5 Pros and Cons of CDuce
+
+6 This work (support for path navigation, using zippers …) Can be used to typecheck XQuery programs
+ I'm gonna focus on 1 in this talk
+
+7 Type algebra
+ Allows to encode regular expression types
+
+8 Semantic subtyping
+
+9 CDuce DataModel
+
+10 CDuce patterns ( Unify typecase and value case, capture variables, destructors, alternation, intersection)
+ Semantics is to return a set of bindings
+ CDuce patterns are typed very precisely
+
+11 Patterns examples : like types but with capture variables
+ Exhaustiveness check
+ So we have this nice functional languages, how to navigate (with upward axes)
+
+12 What are zippers
+
+13 Example of zippers and basic operations
+
+14 Zipper types recursive too, which allows to write reg exps.
+
+15 Already we can check complex conditions
+
+16 Operators & Accumulators
+
+17 Some operators, we'll see why we want them to be built-in
+
+18 Simplified, pattern matching semantics. Only a few rules.
+
+19 Typing patterns with accumulators need approximation
+
+20 Typing patterns with accumulators using accumulators
+
+21 Results
+
+22 Encoding XPath Downward
+ Self
+ Child applied to some document (root, unfold regular expression and try alternatives)
+ Returns this binding, with zippers inside!
+ descendant-or-self (recursively apply child). We update zippers
+ but we dont use them!
+
+23 Binary tree coding
+
+24 Upward Axis
+ Parent : current node is e
+ First walk up and check that it's someone's left child
+ Then walk backwards to skip the previous siblings
+ Then finaly capture the parent