Fixed Points of Type Constructors and Primitive Recursion, Computer Science Logic, 18th International Workshop, vol.3210, pp.190-204, 2004. ,
Git repository of code supplementing the present paper, pp.2018-2019 ,
Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur, 1972. ,
Proofs and types, Cambridge Tracts in Theoretical Computer Science, vol.7, 1989. ,
Parametricity and variants of Girard's J operator, Information Processing Letters, vol.70, pp.1-5, 1999. ,
Non Strictly Positive Datatypes in System F, Email on types mailing list, 1993. ,
Approaches to Recursive Datatypes -a Case Study, 1995. ,
Linear-time Breadth-first Tree Algorithms: An Exercise in the Arithmetic of Folds and Zips, 1993. ,
, Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types. Doktorarbeit (PhD thesis), 1998.
Tarski's fixed-point theorem and lambda calculi with monotone inductive types, Synthese, vol.133, issue.1, pp.107-129, 2002. ,
Inductive Definition in Type Theory, 1987. ,
Simple and Efficient Purely Functional Queues and Deques, J. Funct. Program, vol.5, issue.4, pp.583-592, 1995. ,
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. ,