相关论文: A type-based termination criterion for dependently…

We study the properties, in particular termination, of dependent types systems for lambda calculus and rewriting.

In a previous work, the first author extended to higher-order rewriting and dependent types the use of size annotations in types, a termination proof technique called type or size based termination and initially developed for ML-like…

We provide a general and modular criterion for the termination of simply-typed $\lambda$ -calculus extended with function symbols defined by user-defined rewrite rules. Following a work of Hughes, Pareto and Sabry for functions defined with…

We study the termination of rewriting modulo a set of equations in the Calculus of Algebraic Constructions, an extension of the Calculus of Constructions with functions and predicates defined by higher-order rewrite rules. In a previous…

This paper describes an automatic termination checker for a generic first-order call-by-value language in ML style. We use the fact that value are built from variants and tuples to keep some information about how arguments of recursive call…

Dependency pairs are a key concept at the core of modern automated termination provers for first-order term rewriting systems. In this paper, we introduce an extension of this technique for a large class of dependently-typed higher-order…

In this paper, we show how to extend the notion of reducibility introduced by Girard for proving the termination of $\beta$-reduction in the polymorphic $\lambda$-calculus, to prove the termination of various kinds of rewrite relations on…

We introduce a new formulation of the axiom of dependent choice that can be viewed as an abstract termination principle, which generalises the recursive path orderings used to establish termination of rewrite systems. We consider several…

Since Val Tannen's pioneer work on the combination of simply-typed lambda-calculus and first-order rewriting (LICS'88), many authors have contributed to this subject by extending it to richer typed lambda-calculi and rewriting paradigms,…

In sequential functional languages, sized types enable termination checking of programs with complex patterns of recursion in the presence of mixed inductive-coinductive types. In this paper, we adapt sized types and their metatheory to the…

We revisit the static dependency pair method for proving termination of higher-order term rewriting and extend it in a number of ways: (1) We introduce a new rewrite formalism designed for general applicability in termination proving of…

The main novelty of this paper is to consider an extension of the Calculus of Constructions where predicates can be defined with a general form of rewrite rules. We prove the strong normalization of the reduction relation generated by the…

Rewriting is a framework for reasoning about functional programming. The dependency pair criterion is a well-known mechanism to analyze termination of term rewriting systems. Functional specifications with an operational semantics based on…

The Size-Change Termination principle was first introduced to study the termination of first-order functional programs. In this work, we show that it can also be used to study the termination of higher-order rewriting in a system of…

Refinement types are a well-studied manner of performing in-depth analysis on functional programs. The dependency pair method is a very powerful method used to prove termination of rewrite systems; however its extension to higher order…

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…

Some type-based approaches to termination use sized types: an ordinal bound for the size of a data structure is stored in its type. A recursive function over a sized type is accepted if it is visible in the type system that recursive calls…

This paper proposes a type-and-effect system called Teqt, which distinguishes terminating terms and total functions from possibly diverging terms and partial functions, for a lambda calculus with general recursion and equality types. The…

We propose a generic termination proof method for rewriting under strategies, based on an explicit induction on the termination property. Rewriting trees on ground terms are modeled by proof trees, generated by alternatively applying…

The expressiveness of dependent type theory can be extended by identifying types modulo some additional computation rules. But, for preserving the decidability of type-checking or the logical consistency of the system, one must make sure…