Research software

Query processing Graph data Neuro-symbolic AI Static analysis Predictive analytics

MuIR

Algebraic foundations for optimizing recursion

MuIR is an extensible query compiler and optimizer that turns recursive graph queries into efficient executable plans for relational backends, making previously impractical queries feasible.

Scientific contribution. MuIR addresses a fundamental gap in modern data systems: supporting recursion is not the same as optimizing it. Its recursive relational algebra makes fixpoints first-class optimization objects, so that joins, filters, projections, and interacting recursions can be reorganized across recursive boundaries. A factorized plan representation compactly captures large families of equivalent recursive plans and enables their efficient enumeration and cost-based selection.

Practical relevance and impact. MuIR separates graph-query semantics from backend-specific execution. It accepts navigational queries over knowledge graphs and property graphs, optimizes them through a common algebraic intermediate representation, and emits executable target code, notably SQL for PostgreSQL. Rather than introducing another specialized graph engine, it makes state-of-the-art recursive-query optimization available to existing data platforms. Experiments underlying the system show that, on the evaluated workloads, the quality of the recursive plan can be more decisive than the choice of a specialized storage or execution engine. In some cases, the plans generated by MuIR outperform state-of-the-art systems by several orders of magnitude, turning previously impractical query evaluations into feasible computations.

Its foundations and core optimization methods were published at SIGMOD, VLDB, ICDE and PACMMOD.

Open source Query optimization Graph data

Illustration of the MuIR plan space for recursive graph queries

Plan-space exploration for recursive graph queries

Example of a recursive query plan produced by MuIR

Example query plan

Tree Reasoning Solver

Expressive and efficient reasoning over finite trees

The Tree Reasoning Solver turns a major result in computational logic into a practical reasoning engine.

Scientific contribution. At its core is a modal fixpoint logic over finite trees, equipped with converse modalities, nominals, full negation, and n-ary fixpoints for expressing mutual recursion. At the level of definable tree properties, the logic has the same expressive power as monadic second-order logic (MSO). Yet, whereas direct reasoning in MSO has non-elementary worst-case complexity in the size of the formula, satisfiability for this logic is EXPTIME-complete and can be decided in single-exponential time, 2^O(n). This yields a distinctive combination of expressive power, succinctness, optimal worst-case complexity, and practical effectiveness. The decision procedure is implemented using symbolic techniques based on Binary Decision Diagrams, making sophisticated logical reasoning effective on realistic static analysis problems.

Applications and impact. The solver has been used in research projects worldwide: at the University of Washington for query intersection in Web-script analysis; at the University of Maryland and FORTH for access-control policies and document security; at the University of Edinburgh for XML query containment; at the University of British Columbia for cloud-software analysis; and at the University of Stuttgart for the analysis of BPEL data flows. In my group, we used it to solve a problem that had remained open for more than 10 years in the programming language community. We proved the decidability of subtyping for a very rich type algebra (see our ICFP and TOPLAS papers). We also used it to introduce, for the first time, static analyses for cascading style sheets (see our WWW paper) and more generally queries over structured data.

The theoretical foundations and applications of the system were published at PLDI, TOCL, IJCAI, AAAI, ICFP, and TOPLAS, among others.

Online demo MSO expressiveness EXPTIME-optimal procedure

Architecture of the Tree Reasoning Solver

Solver architecture

Web interface of the Tree Reasoning Solver

Online interface

Additional Research Software

Applied prototypes developed to validate scientific ideas and connect research methods with real-world data.

Illustration of a MedAnalytics research notebook

Predictive analytics Health data

MedAnalytics notebooks

Research notebooks for predictive modeling from large-scale electronic health records.

MedAnalytics implements scalable pipelines for analyzing fine-grained clinical and medication data, with applications to the early identification of patients at risk. The work demonstrates how predictive models can exploit both the volume and the structural richness of real-world health data while requiring only limited information for each patient.

Screenshot of the Adesign image-editing software

Earlier software development

Before entering academic research, I designed and developed end-user software distributed internationally. In 1996, I created WCK, one of the first French web-page editors. I later founded Pierresoft and developed Adesign, a layered image-editing and photo-retouching application licensed and marketed in France, Germany, and Canada.

These early projects gave me an early taste for the full innovation cycle: turning ideas into robust software, bringing them to users, and learning from real-world adoption.