The maximality of the typed lambda calculus and of cartesian closed categories
Théorème de Church-Rosser et structuration des langues naturelles
Two extensions of system F with (co)iteration and primitive (co)recursion principles
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....