Related papers: Definitions by rewriting in the Calculus of Constr…

Term rewriting systems have a simple syntax and semantics and facilitate proofs of correctness. However, they are not as popular in industry or academia as imperative languages. We define a term rewriting based abstract programming language…

In this paper we formalize some foundation concepts and theorems of group theory in a variant of type theory called the Calculus of Constructions with Definitions. In this theory we introduce definition of a group, which is both general and…

Argumentation is the process of constructing arguments about propositions, and the assignment of statements of confidence to those propositions based on the nature and relative strength of their supporting arguments. The process is modelled…

Rewriting techniques based on reduction orderings generate "just enough" consequences to retain first-order completeness. This is ideal for superposition-based first-order theorem proving, but for at least one approach to inductive…

Logically constrained term rewriting is a relatively new formalism where rules are equipped with constraints over some arbitrary theory. Although there are many recent advances with respect to rewriting induction, completion, complexity…

In the last few years appeared pedagogical propositional natural deduction systems. In these systems, one must satisfy the pedagogical constraint: the user must give an example of any introduced notion. First we expose the reasons of such a…

Adding rewriting to a proof assistant based on the Curry-Howard isomorphism, such as Coq, may greatly improve usability of the tool. Unfortunately adding an arbitrary set of rewrite rules may render the underlying formal system undecidable…

This paper is an expository contribution reporting on published work. It focusses on an approach followed in the rewriting community to formalize the concept of strategy. Based on rewriting concepts, several definitions of strategy are…

Many automatic theorem-provers rely on rewriting. Using theorems as rewrite rules helps to simplify the subgoals that arise during a proof. LCF is an interactive theorem-prover intended for reasoning about computation. Its implementation of…

In the research on computational effects, defined algebraically, effect symbols are often expected to obey certain equations. If we orient these equations, we get a rewrite system, which may be an effective way of transforming or optimizing…

This paper introduces a new term rewriting system that is similar to the embedded read-back mechanism for interaction nets presented in our previous work, but is easier to follow than in the original setting and thus to analyze its…

Rewriting logic is naturally concurrent: several subterms of the state term can be rewritten simultaneously. But state terms are global, which makes compositionality difficult to achieve. Compositionality here means being able to decompose…

A non-deterministic call-by-need lambda-calculus \calc with case, constructors, letrec and a (non-deterministic) erratic choice, based on rewriting rules is investigated. A standard reduction is defined as a variant of left-most outermost…

Non-confluent and non-terminating constructor-based term rewrite systems are useful for the purpose of specification and programming. In particular, existing functional logic languages use such kind of rewrite systems to define possibly…

We introduce a class of rooted graphs which allows one to encode various kinds of classical or quantum circuits. We then follow a set-theoretic approach to define rewrite systems over the considered graphs and propose a new complete…

Refinement types are types equipped with predicates that specify preconditions and postconditions of underlying functional languages. We propose a general semantic construction of dependent refinement type systems from underlying type…

Probabilistic programming is becoming increasingly popular thanks to its ability to specify problems with a certain degree of uncertainty. In this work, we focus on term rewriting, a well-known computational formalism. In particular, we…

We propose a functional description of rewriting systems on topological vector spaces. We introduce the topological confluence property as an approximation of the confluence property. Using a representation of linear topological rewriting…

This paper concerns the explicit treatment of substitutions in the lambda calculus. One of its contributions is the simplification and rationalization of the suspension calculus that embodies such a treatment. The earlier version of this…

Proof terms are syntactic expressions that represent computations in term rewriting. They were introduced by Meseguer and exploited by van Oostrom and de Vrijer to study equivalence of reductions in (left-linear) first-order term rewriting…