Two extensions of system with (co)iteration and primitive (co)recursion principles

Issue		RAIRO-Theor. Inf. Appl. Volume 43, Number 4, October-December 2009


Page(s)		703 - 766
DOI		10.1051/ita/2009015
Published online		01 September 2009

RAIRO-Theor. Inf. Appl. 43 (2009) 703-766
DOI: 10.1051/ita/2009015

Two extensions of system ${\mathsf F}$ with (co)iteration and primitive (co)recursion principles

Favio Ezequiel Miranda-Perea

Departamento de Matemáticas, Facultad de Ciencias UNAM, Circuito Exterior S/N. Ciudad Universitaria, 04510 México, D.F. México; favio@ciencias.unam.mx

Received February 2nd, 2007. Accepted July 16, 2009. Published online 1 September 2009

Abstract
This paper presents two extensions of the second order polymorphic lambda calculus, system ${\mathsf F}$ , with monotone (co)inductive types supporting (co)iteration, primitive (co)recursion and inversion principles as primitives. One extension is inspired by the usual categorical approach to programming by means of initial algebras and final coalgebras; whereas the other models dialgebras, and can be seen as an extension of Hagino's categorical lambda calculus within the framework of parametric polymorphism. The systems are presented in Curry-style, and are proven to be terminating and type-preserving. Moreover their expressiveness is shown by means of several programming examples, going from usual data types to lazy codata types such as streams or infinite trees.

Mathematics Subject Classification. 03B40, 68N18, 68Q42, 68Q65

Key words: Coiteration -- corecursion -- iteration -- primitive recursion -- system F -- monotone inductive type -- monotone coinductive type -- monotonicity witness -- saturated sets -- algebras -- coalgebras -- dialgebras.

© EDP Sciences 2009

What is OpenURL?

The OpenURL standard is a protocol for transmission of metadata describing the resource that you wish to access. An OpenURL link contains article metadata and directs it to the OpenURL server of your choice. The OpenURL server can provide access to the resource and also offer complementary services (specific search engine, export of references...). The OpenURL link can be generated by different means.

If your librarian has set up your subscription with an OpenURL resolver, OpenURL links appear automatically on the abstract pages.
You can define your own OpenURL resolver with your EDPS Account. In this case your choice will be given priority over that of your library.
You can use an add-on for your browser (Firefox or I.E.) to display OpenURL links on a page (see http://www.openly.com/openurlref/). You should disable this module if you wish to use the OpenURL server that you or your library have defined.