Related papers: Coinductive Foundations of Infinitary Rewriting an…
We introduce a coinductive definition of infinitary term rewriting. The setup is surprisingly simple, and has in contrast to the usual definitions of infinitary rewriting, neither need for ordinals nor for metric convergence. While the idea…
We present a coinductive framework for defining infinitary analogues of equational reasoning and rewriting in a uniform way. We define the relation =^infty, notion of infinitary equational reasoning, and ->^infty, the standard notion of…
We introduce a generic presentation of 'syntactic objects built by mixed induction and coinduction' encompassing all standard kinds of infinitary terms, as well as derivation trees in non-wellfounded proof systems. We then define a notion…
We introduce an operational rewriting-based semantics for strictly positive nested higher-order (co)inductive types. The semantics takes into account the "limits" of infinite reduction sequences. This may be seen as a refinement and…
We introduce a generalized notion of inference system to support more flexible interpretations of recursive definitions. Besides axioms and inference rules with the usual meaning, we allow also coaxioms, which are, intuitively, axioms which…
Coinductive reasoning about infinitary structures such as streams is widely applicable. However, practical frameworks for developing coinductive proofs and finding reasoning principles that help structure such proofs remain a challenge,…
Inference systems are a widespread framework used to define possibly recursive predicates by means of inference rules. They allow both inductive and coinductive interpretations that are fairly well-studied. In this paper, we consider a…
Coinduction occurs in two guises in Horn clause logic: in proofs of circular properties and relations, and in proofs involving construction of infinite data. Both instances of coinductive reasoning appeared in the literature before, but a…
Coinduction occurs in two guises in Horn clause logic: in proofs of self-referencing properties and relations, and in proofs involving construction of (possibly irregular) infinite data. Both instances of coinductive reasoning appeared in…
Logical frameworks provide natural and direct ways of specifying and reasoning within deductive systems. The logical framework LF and subsequent developments focus on finitary proof systems, making the formalization of circular proof…
We introduce a sound and complete coinductive proof system for reachability properties in transition systems generated by logically constrained term rewriting rules over an order-sorted signature modulo builtins. A key feature of the…
We propose abstract compilation for precise static type analysis of object-oriented languages based on coinductive logic programming. Source code is translated to a logic program, then type-checking and inference problems amount to queries…
In many instances in first order logic or computable algebra, classical theorems show that many problems are undecidable for general structures, but become decidable if some rigidity is imposed on the structure. For example, the set of…
This paper develops an algorithmic-based approach for proving inductive properties of propositional sequent systems such as admissibility, invertibility, cut-elimination, and identity expansion. Although undecidable in general, these…
The purpose of this paper is to develop and study recursive proofs of coinductive predicates. Such recursive proofs allow one to discover proof goals in the construction of a proof of a coinductive predicate, while still allowing the use of…
Term graph rewriting provides a formalism for implementing term rewriting in an efficient manner by avoiding duplication. Infinitary term rewriting has been introduced to study infinite term reduction sequences. Such infinite reductions can…
Recursive definitions of predicates are usually interpreted either inductively or coinductively. Recently, a more powerful approach has been proposed, called flexible coinduction, to express a variety of intermediate interpretations,…
Inductive and coinductive specifications are widely used in formalizing computational systems. Such specifications have a natural rendition in logics that support fixed-point definitions. Another useful formalization device is that of…
We introduce a linear infinitary $\lambda$-calculus, called $\ell\Lambda_{\infty}$, in which two exponential modalities are available, the first one being the usual, finitary one, the other being the only construct interpreted…
Coinduction refers to both a technique for the definition of infinite streams, so-called codata, and a technique for proving the equality of coinductively specified codata. This article first reviews coinduction in declarative programming.…