-
Termination of higher-order rewrite systems based on the notion of computabil...
In this paper, we show how the notion of computability introduced by W. W. Tait and extended to polymorphic types by J.-Y. Girard can be used and easily extended to... -
Modular Aspects of Rewrite-Based Specifications
We investigate modular properties of term rewriting systems, the basic operational formalism for equational specifications. First we study sufficient conditions for... -
On Semi-Completeness of Term Rewriting Systems
We investigate the question whether semi-completeness, i.e., weak termination plus confluence, of term rewriting systems is preserved under the normalization of... -
Decidable Approximations of Sets of Descendants and Sets of Normal Forms - ex...
We present here decidable approximations of sets of descendants and sets of normal forms of Term Rewriting Systems, based on specific tree automata techniques. In the... -
Proving inductive equalities algorithms and implementation
The aim of this paper is first to describe an algorithm for testing sufficient completeness and second to present concepts necessary to understand the behavior of an... -
Automated verification of termination certificates
National audience -
Modular termination of C programs
In this paper we describe a general method to prove termination of C programs in a scalable and modular way. The program to analyse is reduced to the smallest relevant... -
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... -
(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... -
Termination orders for 3-polygraphs
This note presents the first known class of termination orders for 3-polygraphs, together with an application. -
Termination orders for 3-dimensional rewriting
This paper studies 3-polygraphs as a framework for rewriting on two-dimensional words. A translation of term rewriting systems into 3-polygraphs with explicit... -
CoLoR: a Coq library on rewriting and termination
International audience -
Termination of Linear Bounded Term Rewriting Systems
International audience -
V2O3(0001)/Au(111) and /W(110): Growth, Electronic Structure and Adsorption P...
In this work, we firstly showed that it is possible to grow thin<br />V2O3(0001) films on Au(111) and W(110). The preparation process<br />consists of an... -
The Heart of Intersection Type Assignment
This paper gives a new proof for the approximation theorem and the characterisation of normalisability using intersection types. The technique applied is to define... -
RPO constraint solving is in NP
Colloque avec actes et comité de lecture.
