Proof-carrying code provides a mechanism for insuring that a host, or code consumer, can safely run code delivered by a code producer. The host specifies a safety policy as a set ...
Abstract. For narrowing to be an efficient evaluation mechanism, several lazy narrowing strategies have been proposed, although typically for the restricted case of left-linear con...
We present constructive arithmetic in Deduction modulo with rewrite rules only. In natural deduction and in sequent calculus, the cut elimination theorem and the analysis of the st...
Abstract. We show that the structures of binding algebras and Σmonoids by Fiore, Plotkin and Turi are sound and complete models of Klop’s Combinatory Reduction Systems (CRSs). T...
A convenient method for defining a quasi-ordering, such as those used for proving termination of rewriting, is to choose the minimum of a set of quasi-orderings satisfying some d...
Abstract. As a window into the subject, we recount some of the history (and geography) of two mature, challenging, partially open, partially closed problems in the theory of rewrit...
Abstract In order to extend the modeling capabilities of rewriting systems, it is rather natural to consider that the firing of rules can be subject to some probabilistic laws. Co...
In this paper, we consider the monadic second order logic (MSO) and two of its extensions, namely Counting MSO (CMSO) and Presburger MSO (PMSO), interpreted over unranked and unord...