Sciweavers

RTA
2005
Springer
13 years 10 months ago
A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code
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 ...
Amy P. Felty
RTA
2005
Springer
13 years 10 months ago
Natural Narrowing for General Term Rewriting Systems
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...
Santiago Escobar, José Meseguer, Prasanna T...
RTA
2005
Springer
13 years 10 months ago
Arithmetic as a Theory Modulo
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...
Gilles Dowek, Benjamin Werner
RTA
2005
Springer
13 years 10 months ago
Tyrolean Termination Tool
Nao Hirokawa, Aart Middeldorp
RTA
2005
Springer
13 years 10 months ago
Universal Algebra for Termination of Higher-Order Rewriting
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...
Makoto Hamana
RTA
2005
Springer
13 years 10 months ago
Leanest Quasi-orderings
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...
Nachum Dershowitz, E. Castedo Ellerman
RTA
2005
Springer
13 years 10 months ago
Open. Closed. Open
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...
Nachum Dershowitz
RTA
2005
Springer
13 years 10 months ago
Proving Positive Almost-Sure Termination
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...
Olivier Bournez, Florent Garnier
RTA
2005
Springer
13 years 10 months ago
Automata and Logics for Unranked and Unordered Trees
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...
Iovka Boneva, Jean-Marc Talbot
RTA
2005
Springer
13 years 10 months ago
Abstract Modularity
Michael Abbott, Neil Ghani, Christoph Lüth