Typeful certified XML: : integrating language, logic, and data- oriented best practices

The goal of this project is to produce a new generation of
XML programming languages stemming from the synergy of integrating
three approaches into a unique framework: a logical approach, a
data-oriented approach and a programming language
approach. Languages whose constructions are inspired by the latest
results in the PL research; with precise and polymorphic type
systems that merge PL typing techniques with logical-solver-based
type inference; with efficient implementations issued by latest
researches on tree automata and formally certified by latest theorem
prover technologies; with optimizations directly issued from their
types systems and the logical formalizations and whose efficiency
will be formally guaranteed; with the capacity to specify and
formally verify invariants, business rules, and data
integrity. Languages with a direct and immediate impact on
standardization processes.

Research activities
  Data centric languages and systems
  Formalisation of (Specification and Programming) Languages in Proof Assistants
  Data-Centric Languages and Systems

Participants
BENZAKEN Véronique
NGUYEN Kim


More information : http://typex.lri.fr/