.
authorKim Nguyễn <kn@lri.fr>
Tue, 14 Apr 2015 09:32:27 +0000 (11:32 +0200)
committerKim Nguyễn <kn@lri.fr>
Tue, 14 Apr 2015 09:32:27 +0000 (11:32 +0200)
pres-esop15/01.xhtml
pres-esop15/notes.txt [new file with mode: 0644]

index e1e432e..fe24755 100644 (file)
     <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 &setminus; t</mark>  |  <mark>&top;</mark>  |  <mark>&bottom;</mark>  |  &alpha;
+<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 &setminus; t</mark>  |  <mark>&top;</mark>  |  <mark>&bottom;</mark>  |  &alpha;
 </pre>
 <p><dfn>b</dfn> : ranges over basic types (<tt>Int</tt>, <tt>String</tt>, …)<br/>
    <dfn>c</dfn> : ranges over singleton types
diff --git a/pres-esop15/notes.txt b/pres-esop15/notes.txt
new file mode 100644 (file)
index 0000000..9c726d7
--- /dev/null
@@ -0,0 +1,69 @@
+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