Related papers: A type-based termination criterion for dependently…
Rewriting is a formalism widely used in computer science and mathematical logic. The classical formalism has been extended, in the context of functional languages, with an order over the rules and, in the context of rewrite based languages,…
This paper presents general syntactic conditions ensuring the strong normalization and the logical consistency of the Calculus of Algebraic Constructions, an extension of the Calculus of Constructions with functions and predicates defined…
The lambda-Pi-calculus Modulo is a variant of the lambda-calculus with dependent types where beta-conversion is extended with user-defined rewrite rules. It is an expressive logical framework and has been used to encode logics and type…
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…
This paper presents preliminary work on a general system for integrating dependent types into substructural type systems such as linear logic and linear type theory. Prior work on this front has generally managed to deliver type systems…
We investigate the relationship between two independently developed termination techniques. On the one hand, sized-types based termination (SBT) uses types annotated with size expressions and Girard's reducibility candidates, and applies on…
Several types of term rewriting systems can be distinguished by the way their rules overlap. In particular, we define the classes of prefix, suffix, bottom-up and top-down systems, which generalize similar classes on words. Our aim is to…
On the one hand, checking specific termination proofs by hand, say using a particular collection of matrix interpretations, can be an arduous and error-prone task. On the other hand, automation of such checks would save time and help to…
We develop a class of algebraic interpretations for many-sorted and higher-order term rewriting systems that takes type information into account. Specifically, base-type terms are mapped to \emph{tuples} of natural numbers and higher-order…
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…
Targeting to use contract-based design for the specification and refinement of extra-functional properties, this research abstract suggests to use type constraints and dependent types to ensure correct and consistent top-down decomposition…
While a mature body of work supports the study of rewriting systems, abstract tools for Probabilistic Rewriting are still limited. In this paper we study the question of uniqueness of the result (unique limit distribution), and develop a…
The termination method of weakly monotonic algebras, which has been defined for higher-order rewriting in the HRS formalism, offers a lot of power, but has seen little use in recent years. We adapt and extend this method to the alternative…
On the topic of probabilistic rewriting, there are several works studying both termination and confluence of different systems. While working with a lambda calculus modelling quantum computation, we found a system with probabilistic…
Logically Constrained Term Rewriting Systems (LCTRSs) provide a general framework for term rewriting with constraints. We discuss a simple dependency pair approach to prove termination of LCTRSs. We see that existing techniques transfer to…
We study the termination problem for probabilistic term rewrite systems. We prove that the interpretation method is sound and complete for a strengthening of positive almost sure termination, when abstract reduction systems and term rewrite…
Termination is a central property in sequential programming models: a term is terminating if all its reduction sequences are finite. Termination is also important in concurrency in general, and for message-passing programs in particular. A…
We show how (well-established) type systems based on non-idempotent intersection types can be extended to characterize termination properties of functional programming languages with pattern matching features. To model such programming…
All current investigations to analyze the derivational complexity of term rewrite systems are based on a single termination method, possibly preceded by transformations. However, the exclusive use of direct criteria is problematic due to…
We prove that orthogonal constructor term rewrite systems and lambda-calculus with weak (i.e., no reduction is allowed under the scope of a lambda-abstraction) call-by-value reduction can simulate each other with a linear overhead. In…