A. Abel and R. Matthes, Fixed Points of Type Constructors and Primitive Recursion, Computer Science Logic, 18th International Workshop, vol.3210, pp.190-204, 2004.

U. Berger, R. Matthes, and A. Setzer, Git repository of code supplementing the present paper, pp.2018-2019

J. Girard, Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur, 1972.

J. Girard, Proofs and types, Cambridge Tracts in Theoretical Computer Science, vol.7, 1989.

R. Harper and J. C. Mitchell, Parametricity and variants of Girard's J operator, Information Processing Letters, vol.70, pp.1-5, 1999.

M. Hofmann, Non Strictly Positive Datatypes in System F, Email on types mailing list, 1993.

M. Hofmann, Approaches to Recursive Datatypes -a Case Study, 1995.

G. Jones and J. Gibbons, Linear-time Breadth-first Tree Algorithms: An Exercise in the Arithmetic of Folds and Zips, 1993.

R. Matthes and ;. Lmu-münchen, Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types. Doktorarbeit (PhD thesis), 1998.

R. Matthes, Tarski's fixed-point theorem and lambda calculi with monotone inductive types, Synthese, vol.133, issue.1, pp.107-129, 2002.

P. F. Mendler, Inductive Definition in Type Theory, 1987.

C. Okasaki, Simple and Efficient Purely Functional Queues and Deques, J. Funct. Program, vol.5, issue.4, pp.583-592, 1995.

C. Okasaki, Breadth-first numbering: lessons from a small exercise in algorithm design, Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), pp.131-136, 2000.