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