-
How to characterize the language of ground normal forms
Term rewriting systems provide the computer scientists with a language to express functional definitions on complex domains. In such an area, we face the problem to... -
Automated verification of termination certificates
National audience -
Design and implementation of a proof verifying kernel for the λΠ-calculus modulo
In recent years, the emergence of feature rich and mature interactive proof assistants has enabled large formalization efforts of high-profile conjectures and results... -
Kleene algebra, Rewriting modulo AC and Circuits in Coq.
This thesis describe three formalisations in Coq. The first chapter is devoted to the implementation of an efficient decision procedure for Kleene algebras : as... -
Generalized Multisets for Chemical Programming
Gamma is a programming model where computation can be seen as chemical reactions between data represented as molecules floating in a chemical solution. This model can... -
A type system for embedded rewriting programming
In software engineering, type systems are often considered in order to prevent the occurrence of meaningless terms in regard to a type specification. When extending a... -
A Simple Constraint-solving Decision Procedure for Protocols with Exclusive or
We present a procedure for deciding security of protocols employing the Exclusive or operator. This procedure relies on a direct combination of a constraint solver for... -
Theorem Proving Modulo
Projet COQ, Projet PARA, PROTHEO -
Holls: an Intentional First-Order Expression of Higher-Order Logic
Projet COQ, Projet PARA, PROTHEO -
Unification modulo ACUI plus Distributivity Axioms
E-unification problems are central in automated deduction. In this work, we consider unification modulo theories that extend the well-known ACI or ACUI, by adding a... -
Toward a General Rewriting-Based Framework for Reducibility
Reducibility is a powerful proof method which applies to various properties of typed terms in different type systems. For strong normalization, different vari- ants... -
Some General Results About Proof Normalization
International audience -
Governance and Analysis of Business Processes Change Impact on Service Orient...
Most companies evolve in competitive markets by quickly adapting their business processes. Their performance depends on their capability to adopt continuous... -
On the Exploration of the Query Rewriting Space with Existential Rules
We address the issue of Ontology-Based Data Access, with ontologies represented in the framework of existential rules, also known as Datalog+/-. A well-known approach... -
Strengthening the heart of an SMT-solver : Design and implementation of effic...
This thesis tackles the problem of automatically proving the validity of mathematical formulas generated by program verification tools. In particular, it focuses on... -
Letter-to-phoneme conversion by inference of rewriting rules
International audience -
The oulipian ''translator'' : the medieval library of Jacques Roubaud
This thesis examines how the Oulipian Jacques Roubaud, while rewriting texts and motifs from Middle Ages, also recaptures an ancient practice of literature. Indeed,... -
A Sound and Complete Backward Chaining Algorithm for Existential Rules
International audience -
Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo
International audience -
(HO)RPO Revisited
The notion of computability closure has been introduced for proving the termination of the combination of higher-order rewriting and beta-reduction. It is also used...
