相关论文: General Recursion via Coinductive Types

The concept of_refinement_ in type theory is a way of reconciling the "intrinsic" and the "extrinsic" meanings of types. We begin with a rigorous analysis of this concept, settling on the simple conclusion that the type-theoretic notion of…

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…

This paper proposes a definition of recognizable transducers over monads and comonads, which bridges two important ongoing efforts in the current research on regularity. The first effort is the study of regular transductions, which extends…

Constructive type theory combines logic and programming in one language. This is useful both for reasoning about programs written in type theory, as well as for reasoning about other programming languages inside type theory. It is…

Graded monads refine traditional monads using effect annotations in order to describe quantitatively the computational effects that a program can generate. They have been successfully applied to a variety of formal systems for reasoning…

We introduce a category-theoreticabstraction of a syntax with auxiliary functions, called an admissiblemonad morphism. Relying on an abstract form of structural recursion,we then design generic tools to construct admissible monad…

This paper studies fundamental questions concerning category-theoretic models of induction and recursion. We are concerned with the relationship between well-founded and recursive coalgebras for an endofunctor. For monomorphism preserving…

This article contains a proposal to add coinduction to the computational apparatus of natural language understanding. This, we argue, will provide a basis for more realistic, computationally sound, and scalable models of natural language…

For every partial combinatory algebra (pca) $A$ and every partial endofunction on $A$, a pca $A[f]$ is constructed such that in $A[f]$, the function $f$ is representable by an element; a universal property of the construction is formulated…

We construct a model of type theory enjoying parametricity from an arbitrary one. A type in the new model is a semi-cubical type in the old one, illustrating the correspondence between parametricity and cubes. Our construction works not…

The powers of generating functions and its properties are analyzed. A new class of functions is introduced, based on the application of compositions of an integer $n$, called composita. The methods for obtaining reciprocal and reverse…

We present an elaboration of inductive definitions down to a universe of datatypes. The universe of datatypes is an internal presentation of strictly positive families within type theory. By elaborating an inductive definition -- a…

Clocked Type Theory (CloTT) is a type theory for guarded recursion useful for programming with coinductive types, allowing productivity to be encoded in types, and for reasoning about advanced programming language features using an abstract…

Reversible computing is motivated by both pragmatic and foundational considerations arising from a variety of disciplines. We take a particular path through the development of reversible computation, emphasizing compositional reversible…

Containers capture the concept of strictly positive data types in programming. The original development of containers is done in the internal language of locally cartesian closed categories (LCCCs) with disjoint coproducts and W-types, and…

Recursive coalgebras provide an elegant categorical tool for modelling recursive algorithms and analysing their termination and correctness. By considering coalgebras over categories of suitably indexed families, the correctness of the…

Monads are extensively used nowadays to abstractly model a wide range of computational effects such as nondeterminism, statefulness, and exceptions. It turns out that equipping a monad with a (uniform) iteration operator satisfying a set of…

Incremental computation has recently been studied using the concepts of change structures and derivatives of programs, where the derivative of a function allows updating the output of the function based on a change to its input. We…

We exhibit a sound and complete implicit-complexity formalism for functions feasibly computable by structural recursions over inductively defined data structures. Feasibly computable here means that the structural-recursive definition runs…

Ludics is a logical framework in which types/formulas are modelled by sets of terms with the same computational behaviour. This paper investigates the representation of inductive data types and functional types in ludics. We study their…