<div class="sws-slide">
<h1>&cduce;'s type algebra</h1>
<p>A set &mathT; of types</p>
-<pre style="text-align:center;"> t ::= b | c | <u>t × t</u> | <u>t &rarrow; t</u> | <a>t &lor; t</a> | <mark>t &land; t</mark> | <mark>t ∖ t</mark> | <mark>⊤</mark> | <mark>⊥</mark> | α
+<pre style="text-align:center;"> t ::= b | c | <u>t × t</u> | <u>t &rarrow; t</u> | <mark>t &lor; t</mark> | <mark>t &land; t</mark> | <mark>t ∖ t</mark> | <mark>⊤</mark> | <mark>⊥</mark> | α
</pre>
<p><dfn>b</dfn> : ranges over basic types (<tt>Int</tt>, <tt>String</tt>, …)<br/>
<dfn>c</dfn> : ranges over singleton types
--- /dev/null
+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