| Issue |
RAIRO-Theor. Inf. Appl.
Volume 43, Number 4, October-December 2009
|
|
|---|---|---|
| Page(s) | 703 - 766 | |
| DOI | https://doi.org/10.1051/ita/2009015 | |
| Published online | 01 September 2009 | |
Two extensions of system F with (co)iteration and primitive (co)recursion principles
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:
2
February
2007
Accepted:
16
July
2009
This paper presents two extensions of the second order polymorphic lambda calculus, system 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
Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.
Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.
Initial download of the metrics may take a while.