N° | Title | Kind | Delivery date | Participants | ||
Planned | Rescheduled | Delivered | ||||
Constraint generation for inferring types in polymorphic function application with semantic subtyping | Report | M12 | LRI, PPS | |||
Type synthesis for the logical solver | Report | M12 | LRI, PPS, WAM | |||
D.2.c | Resolution of sets of constraints by means of an extended logical solver | Report | M21 | Part 1: logic-based subtyping algo | LRI, PPS, WAM | |
Part 2: ad hoc local type inference algo | ||||||
D.2.d | Design and implementation of the extension of ℂDuce with polymorphic functions | Report | M30 | Part 1: implementation techniques | LRI, PPS | |
Part 2: release | ||||||
D.3.a | SXSI™ with backward axes | Prototype | M21 | M18 (code) | LRI | |
D.3.b | Coq libraries for XPath and alternating tree automata manipulation | Prototype | M15 | M22 | M22 | LRI, PPS, WAM |
D.3.c | Formal proof of SXSI™ core | Report | M24 | M24 | PPS, LRI | |
D.3.d | Automated proofs for the solver | M30 | WAM | |||
D.4.a | XQuery equipped with static type system | Report | M24 | Part 1: logic-based | LRI, PPS, WAM | |
Part 2: inference-based | ||||||
D.4.b | XQuery equipped with semantic annotations | Report | M30 | Part 1: SMT-based | LRI, PPS, WAM | |
Part 2: Schema-based | ||||||
D.4.c | XQuery engine with static type system and logical assertions | Prototype | M36 | LRI, PPS, WAM | ||
D.5.a | Proposal for a standard XML transformation language with pattern matching, polymorphism, assertions, precise type checking, efficient certified implementation | Report | M36 | LRI,PPS,WAM | ||
Formalization of NoSQL Languages | Report | new | LRI, PPS | |||
A set-theoretic type system for polymorphic variants in ML | Report | new | LRI, PPS | |||
M.2.i | Polymorphic types for languages and solvers. | Milestone | M15 | M12 | ||
M.2.ii | Polymorphic functions application | Milestone | M24 | M18 | ||
M.2.iii | Polymorphic ℂDuce | Milestone | M36 | M30 | ||
M.3.i | Handling of backward axes within SXSI™ | Milestone | M21 | M21 | ||
M.3.ii | SXSI™ core functionality is verified. | Milestone | M24 | |||
M.3.iii | SXSI™ with backward axes is verified | Milestone | M36 | |||
M.3.iv | The algorithm of the solver is verified | Milestone | M30 | |||
M.4.i | A functional Core for XQuery 3.0. | Milestone | M12 | M14 | ||
M.4.ii | Type system for XQuery with higher-order functions and pattern matching. | Milestone | M24 | M14 | ||
M.4.iii | Statically verified XQuery assertions. | Milestone | M21 | |||
M.5.i | Fundamentals of XQuery 4.0 | Milestone | M36 | |||
A detailed description of deliverables and milestone can be found in this document