Two extensions of system 𝖥 with (co)iteration and primitive (co)recursion principles
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 43 (2009) no. 4, pp. 703-766.

Voir la notice de l'article dans Numdam

This paper presents two extensions of the second order polymorphic lambda calculus, system 𝖥, 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.

DOI : 10.1051/ita/2009015
Classification : 03B40, 68N18, 68Q42, 68Q65
Mots-clés : coiteration, corecursion, iteration, primitive recursion, system F, monotone inductive type, monotone coinductive type, monotonicity witness, saturated sets, algebras, coalgebras, dialgebras 
@article{ITA_2009__43_4_703_0,
     author = {Miranda-Perea, Favio Ezequiel},
     title = {Two extensions of system ${\mathsf {F}}$ with (co)iteration and primitive (co)recursion principles},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     pages = {703--766},
     publisher = {EDP-Sciences},
     volume = {43},
     number = {4},
     year = {2009},
     doi = {10.1051/ita/2009015},
     mrnumber = {2589990},
     language = {en},
     url = {https://geodesic-test.mathdoc.fr/articles/10.1051/ita/2009015/}
}
TY  - JOUR
AU  - Miranda-Perea, Favio Ezequiel
TI  - Two extensions of system ${\mathsf {F}}$ with (co)iteration and primitive (co)recursion principles
JO  - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY  - 2009
SP  - 703
EP  - 766
VL  - 43
IS  - 4
PB  - EDP-Sciences
UR  - https://geodesic-test.mathdoc.fr/articles/10.1051/ita/2009015/
DO  - 10.1051/ita/2009015
LA  - en
ID  - ITA_2009__43_4_703_0
ER  - 
%0 Journal Article
%A Miranda-Perea, Favio Ezequiel
%T Two extensions of system ${\mathsf {F}}$ with (co)iteration and primitive (co)recursion principles
%J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
%D 2009
%P 703-766
%V 43
%N 4
%I EDP-Sciences
%U https://geodesic-test.mathdoc.fr/articles/10.1051/ita/2009015/
%R 10.1051/ita/2009015
%G en
%F ITA_2009__43_4_703_0
Miranda-Perea, Favio Ezequiel. Two extensions of system ${\mathsf {F}}$ with (co)iteration and primitive (co)recursion principles. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 43 (2009) no. 4, pp. 703-766. doi : 10.1051/ita/2009015. https://geodesic-test.mathdoc.fr/articles/10.1051/ita/2009015/

Cité par Sources :