1,720,992 research outputs found
Antifounded Coinduction in Type Theory
No full textVenanzio Capretta, Varmo Vene and I have previously studied antifounded algebras as a a category-theoretic formulation of antifounded coinduction. These are the dual of wellfounded coalgebras, a category theorist's take on wellfounded induction, closely related to the Bove-Capretta method for justifying function definitions by general recursion in type theory.In this talk, we discuss one possible type-theoretic approach to antifounded coinduction.</jats:p
Universal algebra in type theory
No full textAbstract. We present a development of Universal Algebra inside Type Theory, formalized using the proof assistant Coq. We define the notion of a signature and of an algebra over a signature. We use setoids, i.e. types endowed with an arbitrary equivalence relation, as carriers for algebras. In this way it is possible to define the quotient of an algebra by a congruence. Standard constructions over algebras are defined and their basic properties are proved formally. To overcome the problem of defining term algebras in a uniform way, we use types of trees that generalize wellorderings. Our implementation gives tools to define new algebraic structures, to manipulate them and to prove their properties.
Certifying the fast Fourier transform with Coq
No full textAbstract. We program the Fast Fourier Transform in type theory, using the tool Coq. We prove its correctness and the correctness of the Inverse Fourier Transform. A type of trees representing vectors with interleaved elements is defined to facilitate the definition of the transform by structural recursion. We define several operations and proof tools for this data structure, leading to a simple proof of correctness of the algorithm. The inverse transform, on the other hand, is implemented on a different representation of the data, that makes reasoning about summations easier. The link between the two data types is given by an isomorphism. This work is an illustration of the two-level approach to proof development and of the principle of adapting the data representation to the specific algorithm under study. CtCoq, a graphical user interface of Coq, helped in the development. We discuss the characteristics and usefulness of this tool.
A polymorphic representation of . . .
No full textDybjer’s simultaneous inductive-recursive definitions [3] can be represented in the Calculus of Inductive Constructions by an impredicative Σ-type. The idea was suggested by the presentation of inductive types à la Mendler given by Uustalu and Vene [6], in particular by their example implementation o
A general method to prove the normalization theorem for first and second order typed λ-calculi
No full textand second order typed λ-calcul
Coalgebras in functional programming and type theory
No full textAbstractThis is a survey article on the use of coalgebras in functional programming and type theory. It presents the basic theory underlying the implementation of coinductive types, families and predicates. It gives an overview of the application of corecursive methods to the study of general recursion, formal power series, tabulations of functions on inductive data. It also sketches some advanced topics in the study of the solutions to non-guarded corecursive equations and the design of non-standard type theory
General recursion via coinductive types
No full textA fertile field of research in theoretical computer science investigates the representation of general recursive functions in intensional type theories. Among the most successful approaches are: the use of wellfounded relations, implementation of operational semantics, formalization of domain theory, and inductive definition of domain predicates. Here, a different solution is proposed: exploiting coinductive types to model infinite computations. To every type A we associate a type of partial elements A ν, coinductively generated by two constructors: the first, �a � just returns an element a: A; the second, ⊲ x, adds a computation step to a recursive element x: A ν. We show how this simple device is sufficient to formalize all recursive functions between two given types. It allows the definition of fixed points of finitary, that is, continuous, operators. We will compare this approach to different ones from the literature. Finally, we mention that the formalization, with appropriate structural maps, defines a strong monad
Modelling General Recursion in Type Theory
No full textConstructive type theory is an expressive programming language where both algorithms and proofs can be represented. However, general recursive algorithms have no direct formalisation in type theory since they contain recursive calls that satisfy no syntactic condition guaranteeing termination
- …
