相关论文: General Recursion via Coinductive Types

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…

Category theory is famous for its innovative way of thinking of concepts by their descriptions, in particular by establishing universal properties. Concepts that can be characterized in a universal way receive a certain quality seal, which…

In the pure Calculus of Constructions (CC) one can define data types and function over these, and there is a powerful higher order logic to reason over these functions and data types. This is due to the combination of impredicativity and…

In group representations several inductions given by tensoring with appropriate bimodules may be reconstructed via homology of $G$-posets with $G$-equivariant coefficients. For this purpose, we need various local categories of a finite…

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,…

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…

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…

Reversibility is a key issue in the interface between computation and physics, and of growing importance as miniaturization progresses towards its physical limits. Most foundational work on reversible computing to date has focussed on…

Structured recursion schemes have been widely used in constructing, optimising, and reasoning about programs over inductive and coinductive datatypes. Their plain forms, catamorphisms and anamorphisms, are restricted in expressiveness. Thus…

This article aims to provide a novel formalization of the concept of computational irreducibility in terms of the exactness of functorial correspondence between a category of data structures and elementary computations and a corresponding…

To appear in Theory and Practice of Logic Programming (TPLP). Tabling is a commonly used technique in logic programming for avoiding cyclic behavior of logic programs and enabling more declarative program definitions. Furthermore, tabling…

We define the syntax and reduction relation of a recursively typed lambda calculus with a parallel case-function (a parallel conditional). The reduction is shown to be confluent. We interpret the recursive types as information systems in a…

Disjunctive finitary programs are a class of logic programs admitting function symbols and hence infinite domains. They have very good computational properties, for example ground queries are decidable while in the general case the stable…

The use of a necessity modality in a typed $\lambda$-calculus can be used to separate it into two regions. These can be thought of as intensional vs. extensional data: data in the first region, the modal one, are available as code, and…

The purpose of this paper is to clarify the relationship between various conditions implying essential undecidability: our main result is that there exists a theory $T$ in which all partially recursive functions are representable, yet $T$…

We extend intersection types to a computational $\lambda$-calculus with algebraic operations \`a la Plotkin and Power. We achieve this by considering monadic intersections, whereby computational effects appear not only in the operational…

Neither the classical nor intuitionistic logic traditions are perfectly-aligned with the purpose of reasoning about computation, in that neither tradition can permit unconstrained recursive definitions without inconsistency: recursive…

In a previous work ("Abstract Data Type Systems", TCS 173(2), 1997), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system and a typed lambda-calculus enriched by pattern-matching…

We introduce a framework for online structure theory. Our approach generalises notions arising independently in several areas of computability theory and complexity theory. We suggest a unifying approach using operators where we allow the…

We develop and investigate a general theory of representations of second-order functionals, based on a notion of a right comodule for a monad on the category of containers. We show how the notion of comodule representability naturally…